Copyright | (c) 2014-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- 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
.