Commit f4caeb89 authored by Heiko Becker's avatar Heiko Becker
Browse files

prove new Interval valildation soundness for expressions

parent 1a5a82c0
......@@ -250,8 +250,8 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ fs [eval_exp_cases]
\\ res_tac));
val toREvalVars_def = Define `
toREvalVars (d:num -> mType option) (n:num) : mType option =
val toRMap_def = Define `
toRMap (d:num -> mType option) (n:num) : mType option =
case d n of
| SOME m => SOME M0
| NONE => NONE`;
......
This diff is collapsed.
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