Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
elab
/
lambdaLiftCache.lean
blob: b4bfceb137582f8d572253a32e4f6a15813a53b3 [
file
] [
edit
]
def
map
(
f
:
Nat
→
Nat
)
(
xs
:
List
Nat
)
:=
xs
.
map f
set_option trace
.
Compiler
.
saveMono
true
def
foo
(
x
:
Nat
)
(
xs
:
List
Nat
)
:=
map
(·
+
x
)
xs
def
boo
(
x
:
Nat
)
(
xs
:
List
Nat
)
:=
map
(·
+
x
)
xs