Copyright | (c) 2014-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
TODO: - Putting in a normal form to spot "prove by assumption" - Additional simplification rules, namely various cancelation. - Things like: lg2 e(x) = x, where we know thate is increasing.
- crySimplify :: Prop -> Prop
- crySimplifyMaybe :: Prop -> Maybe Prop
- crySimpPropExpr :: Prop -> Prop
- crySimpPropExprMaybe :: Prop -> Maybe Prop
Simplify a property
crySimplify :: Prop -> Prop Source #
Simplify a property, if possible.
Simplify expressions in a prop
crySimpPropExpr :: Prop -> Prop Source #
Simplify only the Expr parts of a Prop.