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

Add flushToZero definition

parent dd39d141
......@@ -356,6 +356,9 @@ val is64BitEval_def = Define `
(is64BitEval (Downcast m e) = is64BitEval e) /\
(is64BitEval ((Var v):real exp) = T)`;
val flushToZero_def = Define `
flushToZero e E Gamma v m = (eval_exp e E Gamma v m /\ 0 <= abs v /\ abs v <= 0 (* FIXME *) ==> eval_exp e E Gamma 0 m)`;
val typeMap_eq_typeExp = Q.prove(`!e. typeMap Gamma e e = typeExpression Gamma e`,
Induct \\ fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] );
......
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