Merge branch 'smtv2-dont-fail-on-untyped-prover-vars' into 'master'

[why3.git] / examples_in_progress / reals.mlw

module M

  use int.Int
  use real.RealInfix

  let f (x:int) ensures { result = x + 1 } = x + 1

  let g (x:real) ensures { result = -. x +. 1.0 } = -. x +. 1.0

end