Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
474.lean.out.expected
blob: f8f3c36f7be9d74217e28e203db2abf4414fda33 [
file
] [
edit
]
let
y
:=
Nat
.
zero
;
y
.
add y
fun y_1
=>
y
.
add y_1
fun y
=>
Nat
.
add FREE y
fun
(
y
:
Nat
)
=>
Nat
.
add y y
Nat
.
add
?
m y
Nat
.
add
?
m
#0
fun y
=>
(
y
.
add y
).
add y