Commit 21315d44 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Progress on cmd soundness proof

parent 3655c4ff
This diff is collapsed.
......@@ -164,6 +164,14 @@ Proof.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Lemma usedVars_toRExp_compat e:
usedVars (toRExp e) = usedVars e.
Proof.
induction e; simpl; set_tac.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
......@@ -486,7 +494,7 @@ Proof.
*)
(**
We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
(* Definition analysisResult :Type := expr Q -> intv * error. *)
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