Copyright | (c) 2013-2015 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
Documentation
assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop]) Source
Collect fin
and simple <=
constraints in the ord model
Returns Left
if we find a goal which is incompatible with the others.
Otherwise, we return Right
with a model, and the remaining
(i.e., the non-order related) properties.
These sorts of facts are quite useful during type simplification, because they provide information which potentially useful for cancellation (e.g., this variables is finite and not 0)
checkTypeFunction :: TFun -> [Type] -> [Prop] Source