chore(library/init/io): we don't need fix anymore

`partial def` are much more general

library/init/io.lean

@@ -64,16 +64,13 @@ constant Fs.handle : Type := Unit
 namespace Prim
 open Fs
 
-def iterateAux {α β : Type} (f : α → IO (Sum α β)) : (α → IO β) → (α → IO β)
-| rec a :=
+@[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
+| a f :=
   do v ← f a,
   match v with
-  | Sum.inl a := rec a
+  | Sum.inl a := iterate a f
   | Sum.inr b := pure b
 
-@[specialize] def iterate {α β : Type} (a : α) (f : α → IO (Sum α β)) : IO β :=
-fixCore (λ _, throw "deep recursion") (iterateAux f) a
-
 @[extern 2 "lean_io_prim_put_str"]
 constant putStr (s: @& String) : IO Unit := default _
 @[extern 1 "lean_io_prim_get_line"]

tests/playground/fix.lean

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

tests/playground/fix_1.lean

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

tests/playground/fix_with_tuples.lean

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