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

Fix minor flaw for variables. Loading should not perturb values

parent 2b2c010a
......@@ -41,9 +41,8 @@ let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
of the real valued computation by (1 + d)
*)
let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
`(!eps env v delta.
abs delta <= eps ==>
eval_exp eps env (Var v) (perturb (env v) delta)) /\
`(!eps env v.
eval_exp eps env (Var v) (env v)) /\
(!eps env n delta.
abs delta <= eps ==>
eval_exp eps env (Const n) (perturb n delta)) /\
......
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