Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/Array.mapIdx
/
.
/
tests
/
lean
/
coeAttr1.lean
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