why3doc index index


module Test
  use import int.Int
  use import int.EuclideanDivision

let p x = mod x 2 = 0

let rec f e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else
    g (e - 1)

with g e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else
  if p e then f e
  else g (e-1)

let rec g' e =
requires {0 <= e}
variant {e}
  if e = 0 then 1 else
  if p e then if e = 0 then 1 else g' (e-1)
  else g' (e-1)

let rec g'' e =
requires {0 <= e}
variant {e}
  let f e =
  requires {0 <= e}
  if e = 0 then 1 else
    g'' (e - 1)  in

  if e = 0 then 1 else
  if p e then f e
  else g'' (e-1)

end

Generated by why3doc 0.87.3