lean4-htt/tests/playground/fix.lean
Leonardo de Moura 3936b2ba79 chore(library/init/io): we don't need fix anymore
`partial def` are much more general
2019-03-27 12:59:43 -07:00

8 lines
205 B
Text

partial def foo : Nat → Nat → Nat
| 0 a := a
| (n+1) a := foo n a + a + foo n (a+1)
def main (xs : List String) : IO UInt32 :=
let v := foo (xs.head.toNat) 10 in
IO.println (toString v) *>
pure 0