Leeres forall kann wichtig sein..
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 14 Nov 2008 09:45:04 +0000 (09:45 +0000)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 14 Nov 2008 09:45:04 +0000 (09:45 +0000)
Expr.hs

diff --git a/Expr.hs b/Expr.hs
index 529ee97..89aa2e7 100644 (file)
--- a/Expr.hs
+++ b/Expr.hs
@@ -178,8 +178,9 @@ beTrue = And []
 
 -- | Optimize a forall condition
 condition :: [TypedExpr] -> BoolExpr -> BoolExpr -> BoolExpr
--- empty variable list
-condition [] cond concl   = concl
+-- empty condition
+condition [] cond concl   | cond == beTrue
+                          = concl
 -- float out conditions on the right
 condition vars cond (Condition vars' cond' concl')
                          = condition (vars ++ vars') (cond `aand` cond') concl'