Coe ↑ の明示的な指定で違いが出る例

TPiL に載っている例

def Set (α : Type u) := α → Prop
def Set.empty {α : Type u} : Set α := fun _ => False
def Set.mem (a : α) (s : Set α) : Prop := s a
def Set.singleton (a : α) : Set α := fun x => x = a
def Set.union (a b : Set α) : Set α := fun x => a x ∨ b x
notation "{ " a " }" => Set.singleton a
infix:55 " ∪ " => Set.union
def List.toSet : List α → Set α
  | []    => Set.empty
  | a::as => {a} ∪ as.toSet

instance : Coe (List α) (Set α) where
  coe a := a.toSet

def s : Set Nat := {1}
#check s ∪ [2, 3]

-- この x は Set になっている
#check let x := ↑[2, 3]; s ∪ x

-- この x は List のまま
#check let x := [2, 3]; s ∪ x

The issue provides a TPiL Lean example contrasting an explicit Coe conversion with an inferred one. First locate the corresponding example section in the repository and run the three #check cases in Lean. Done means documenting the observed difference and making the intended explanation or example clear to readers.