GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-29 01:45:36 +03:00
Code Issues Projects Releases Wiki Activity

Add a case for Not. Fixes #249.

Browse Source 
This may happen when we check enumerations, because we emit constraints
such as `x /= y`, which ends up looking like `Not (x == y)`.
This commit is contained in:
Iavor S. Diatchki 2015-06-24 11:34:20 -07:00
parent 91ebb1ca2b
commit e7728c2b22
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs
View File

@ -11,6 +11,7 @@ cryDefinedProp prop =
Fin x -> cryDefined x
x :== y -> cryDefined x :&& cryDefined y
x :>= y -> cryDefined x :&& cryDefined y
Not p -> cryDefinedProp p
_ -> panic "cryDefinedProp" [ "Not a simple property:"
, show (ppProp prop)
]