mutual.mlw 507 Bytes
Newer Older
1
module M
2

3
  use import int.Int
4 5 6 7
  use import int.EuclideanDivision

  logic even (x : int) = x = 2 * (div x 2)
  logic odd  (x : int) = x = 2 * (div x 2) + 1
8

9 10 11 12 13
let rec is_even x : bool variant {x} =
  { 0 <= x }
  if x = 0 then True else is_odd (x-1)
  { result=True <-> even x }

14
with is_odd x : bool variant {x} =
15 16 17 18
  { 0 <= x }
  if x = 0 then False else is_even (x-1)
  { result=True <-> odd x }

19
end
20 21 22 23 24 25

(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/mutual"
End: 
*)