Sign in
◑
Theme
fuchsia
/
third_party
/
github.com
/
leanprover
/
lean4
/
refs/heads/upstream/RArray2
/
.
/
tests
/
compiler
/
strictOrSimp.lean
blob: ea135c5015366725dae7cc4f7711f330be7d0a4d [
file
] [
edit
]
partial
def
spin
:
Nat
→
Bool
|
n
=>
spin
(
n
)
@[
inline
]
def
C
:
Nat
:=
0
def
f
(
b
:
Nat
)
:=
if
strictOr
(
C
==
0
)
(
spin b
)
then
"hello"
else
"world"
def
main
(
xs
:
List
String
)
:
IO
Unit
:=
IO
.
println
(
f
0
)