mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
9 lines
206 B
Plaintext
9 lines
206 B
Plaintext
use int.Int
|
|
use real.FromInt
|
|
use real.RealInfix
|
|
use real.Abs
|
|
|
|
goal g1 : from_int 100 = 100.
|
|
goal g2: forall x. -5 <= x <= 5 -> abs (from_int x) <=. 5.
|
|
goal g3: forall x. x <= 5 -> 10. *. from_int x <=. 50.
|