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.