| Copyright | (c) 2014-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell98 |
Cryptol.TypeCheck.Solver.Numeric.Simplify
Description
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.