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`

.