mach.onetime: removed a meaningless comment

parent 60b16cd3
......@@ -13,12 +13,6 @@ module OneTime
val zero (): t
ensures { result.valid }
ensures { result.v = 0 }
(* FIXME: should be a constant?
val function zero : t
ensures { result.valid }
ensures { result.v = 0 }
*)
val succ (x: t) : t
requires { x.valid }
......
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