Commit 65a8b699 authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove unused definition

parent 96493068
......@@ -3,14 +3,6 @@ Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
Definition analysisResult :Type := exp Q -> intv * error.
Definition envApproximatesPrecond (P:nat -> intv) (absenv:analysisResult) :=
forall u:nat,
let (ivlo,ivhi) := P u in
let (absIv,err) := absenv (Param Q u) in
let (abslo,abshi) := absIv in
(abslo <= ivlo /\ ivhi <= abshi)%Q.
Definition precondValidForExec (P:nat->intv) (cenv:nat->R) :=
forall v:nat,
let (ivlo,ivhi) := P v in
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