cryptol-2.4.0: Cryptol: The Language of Cryptography

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

Contents

- Simplify a property
- Simplify expressions in a prop

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.

Synopsis

- 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.

crySimplifyMaybe :: Prop -> Maybe Prop Source #

Simplify a property, if possible.

# Simplify expressions in a prop

crySimpPropExpr :: Prop -> Prop Source #

Simplify only the Expr parts of a Prop.

crySimpPropExprMaybe :: Prop -> Maybe Prop Source #

Simplify only the Expr parts of a Prop. Returns `Nothing` if there were no changes.