Cryptol.TypeCheck.Solve

Documentation

simplifyAllConstraints :: InferM ()

proveImplication :: LQName -> [TParam] -> [Prop] -> [Goal] -> InferM Subst

assumedOrderModel :: OrdFacts -> [Prop] -> Either (OrdFacts, Prop) (OrdFacts, [Prop])

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]