cryptol-2.4.0: Cryptol: The Language of Cryptography

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.

Synopsis

# Simplify a property

Simplify a property, if possible.

Simplify a property, if possible.

# Simplify expressions in a prop

Simplify only the Expr parts of a Prop.

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