cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2015-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.Numeric.Simplify1

Description

Simplification. The rules in this module are all conditional on the expressions being well-defined.

So, for example, consider the formula `P`, which corresponds to `fin e`. `P` says the following:

if e is well-formed, then will evaluate to a finite natural number.

More concretely, consider `fin (3 - 5)`. This will be simplified to `True`, which does not mean that `3 - 5` is actually finite.

# Documentation

propToProp' :: Prop -> I Bool Source #

ppProp' :: I Bool -> Doc Source #