Commit d9fe3880 authored by MARCHE Claude's avatar MARCHE Claude

a bit of cleaning

parent 98be3171
......@@ -256,7 +256,8 @@ pvsbin/
# modules
module M
use import int.Int
let f (x:int) (ghost y:int) : int
ensures { x = y }
= x
let g (z:int) = f z 0
\ No newline at end of file
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