Commit 4a5df15c authored by MARCHE Claude's avatar MARCHE Claude
Browse files

val for EuclideanDivision

parent b41c1802
......@@ -267,9 +267,6 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
TO DISCUSS:
Pourquoi les lemma functions generent un warning ``does not contain any
abstract symbol'' ?
comment mettre a jour l'example bag ? Parametrer par une egalit'e sur
les elements ?
......
......@@ -143,6 +143,15 @@ theory EuclideanDivision
x > 0 ->
mod (x * y + z) x = mod z x
val div (x y:int) : int
requires { y <> 0 }
ensures { result = div x y }
val mod (x y:int) : int
requires { y <> 0 }
ensures { result = mod x y }
end
(** {2 Division by 2}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment