module Collatz;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
collatzNext (n : Nat) : Nat := if (mod n 2 == 0) (div n 2) (3 * n + 1);
collatz : Nat → Nat
| zero := zero
| (suc zero) := suc zero
| n := collatzNext n;
terminating
run (f : Nat → Nat) : Nat → IO
| (suc zero) := printNatLn 1 >> printStringLn "Finished!"
| n := printNatLn n >> run f (f n);
welcome : String :=
"Collatz calculator\n------------------\n\nType a number then ENTER";
resultHeading : String := "Collatz sequence:";
main : IO :=
printStringLn welcome
>> readLn
λ {s := printStringLn resultHeading >> run collatz (stringToNat s)};
Last modified on 2023-10-06 13:21 UTC