Commit 4795737c authored by Heiko Becker's avatar Heiko Becker
Browse files

Add real machine epsilon from daisy

parent 7316a7f7
......@@ -2,6 +2,7 @@
Formalization of the base expression language for the daisy framework
Require Import Coq.Reals.Reals.
Require Import Daisy.realConversion.
Set Implicit Arguments.
Expressions will use binary operators.
......@@ -31,7 +32,7 @@ Inductive exp (V:Type): Type :=
Define the machine epsilon for floating point operations.
FIXME: Currently set to 1.0 instead of the concrete value!
Definition m_eps:R := 1.
Definition machineEpsilon:R := realFromNum 59604645 7 8.
Define a perturbation function to ease writing of basic definitions
Supports Markdown
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