Copyright | (c) 2015-2016 Galois, Inc. |
---|---|

License | BSD3 |

Maintainer | cryptol@galois.com |

Stability | provisional |

Portability | portable |

Safe Haskell | Safe |

Language | Haskell98 |

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.