Commit 68a05f02 authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

[farith2] Setup extraction of assertions

parent f25307fb
......@@ -13,6 +13,8 @@ Module Assert (M : Inhabited).
| false => M.dummy
end.
Extract Inlined Constant assert => "(fun x f -> assert x; f ())".
Lemma assert_spec:
forall (pre : bool) (f : M.t),
pre = true -> assert pre (fun _ => f) = f.
......@@ -76,5 +78,4 @@ Module GenericFloat.
destruct x as [ ? ? ? ? vx ], y as [ ? ? ? ? vy ]; simpl in *; subst.
apply (Bminus m vx vy).
Defined.
End GenericFloat.
End GenericFloat.
\ No newline at end of file
Supports Markdown
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