Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/expose-array-back
/
.
/
tests
/
compile
/
StackOverflowTask.lean
blob: 87e7ab9ddeeb37db746fc47b6e982e39b888b40f [
file
] [
edit
]
partial
def
foo
:
Nat
→
Nat
|
n
=>
foo n
+
1
@[
never_extract
]
def
main
:
IO
Unit
:=
IO
.
println $
Task
.
get
$
Task
.
spawn fun _
=>
foo
0