cryptol-2.3.0: Cryptol: The Language of Cryptography

Copyright(c) 2015-2016 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

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