Commit 9ac65923 authored by Heiko Becker's avatar Heiko Becker

Adapt simple regression test in Coq

parent 92b5700e
......@@ -5,8 +5,9 @@ Definition e3 :expr Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :(nat -> option mType) := fun n =>
if n =? 0 then Some M64 else None.
Definition defVars_additionSimple :(FloverMap.t mType) :=
FloverMap.add (Var Q 0) M64 (FloverMap.empty mType).
Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
......
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