Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/replace
/
.
/
tests
/
lean
/
invalidNamedArgs.lean
blob: 0310bbe72732bd8f39d4c45e7dd90fb20f2b896c [
file
] [
edit
]
def
ex1
(
xs
:
List
Nat
)
:
Nat
:=
xs
.
foldl
(
b
:=
0
)
fun sum x
=>
sum
+
x
def
f
(
a
:
Nat
)
(
flag
:=
true
)
:
Nat
:=
a
+
if
flag
then
1
else
0
def
g
(
a
:
Nat
)
:
Nat
:=
f a
(
flg
:=
false
)