blob: 8c9171fd05ef67d93f8e897e45b887ac24d73a75 [file] [edit]
@[coe] def f (n : Nat) : String :=
toString n
#check f 10
instance : Coe Nat String where
coe := f
def g (n : String) := n
#check fun x : Nat => g x