| 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.Defined
Description
- cryDefinedProp :: Prop -> Prop
- cryDefined :: Expr -> Prop
Documentation
cryDefinedProp :: Prop -> Prop Source #
A condition ensure that the given *basic* proposition makes sense.
cryDefined :: Expr -> Prop Source #
Generate a property ensuring that the expression is well-defined.
This might be a bit too strict. For example, we reject things like
max inf (0 - 1), which one might think would simplify to inf.