diff --git a/examples/three_idem_ring.mlw b/examples/three_idem_ring.mlw index 387cf3eaf1d2632607750aef5050a0424dbe8e47..60a2aa04785e6563fbe7ec455a9a7efaf8440838 100644 --- a/examples/three_idem_ring.mlw +++ b/examples/three_idem_ring.mlw @@ -6,29 +6,24 @@ module ThreeIdempotentRing use int.Int - type t - val constant zero : t - val function (+) t t : t - val function ( *) t t : t - clone import algebra.Ring as R with - type t = t, constant zero = zero, function (+) = (+), function ( *) = ( *), - axiom . + clone export algebra.Ring with + axiom . (** Define multiplication by an integer recursively *) - let rec function mul (x : t) (n : int) : t + let rec ghost function mul (x : t) (n : int) : t requires { n >= 0 } variant { n } = - if n = 0 then zero else x + mul x (n-1) + if n = 0 then pure{zero} else let r = mul x (n-1) in pure {x + r} (** We get lemmas from the why3 library *) - clone import int.Exponentiation as Mul with - type t = t, constant one = zero, - function ( *) = (+), function power = mul, lemma . + clone int.Exponentiation with type t = t, + constant one = zero, function ( * ) = (+), function power = mul, + lemma . -(** {2 General results about unitary rings} *) +(** {2 General results about rings} *) (** First results : *) diff --git a/examples/three_idem_ring/why3session.xml b/examples/three_idem_ring/why3session.xml index 9698c778398d1cc2ae3da6e0ba74f2b9f7845735..b036061681712eee4a7a857d9a7ab0ca8af9d727 100644 --- a/examples/three_idem_ring/why3session.xml +++ b/examples/three_idem_ring/why3session.xml @@ -13,19 +13,19 @@ - + - + - + - + - + @@ -67,11 +67,9 @@ - - @@ -143,14 +141,14 @@ - + - + @@ -171,7 +169,7 @@ - + diff --git a/examples/three_idem_ring/why3shapes.gz b/examples/three_idem_ring/why3shapes.gz index c6226f92be8414ca69fd52506a8bac8924cff8cf..d4cc58263ce13f4cad084a748846772197439f43 100644 Binary files a/examples/three_idem_ring/why3shapes.gz and b/examples/three_idem_ring/why3shapes.gz differ