cryptol-2.4.0: Cryptol: The Language of Cryptography

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

Synopsis

- 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`.