Cryptol.TypeCheck.Solver.Improve

Look for opportunity to solve goals by instantiating variables.

Documentation

improveProps :: Bool -> Ctxt -> [Prop] -> Match (Subst, [Prop])

Improvements from a bunch of propositions. Invariant: the substitions should be already applied to the new sub-goals, if any.

improveProp :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])

Improvements from a proposition. Invariant: the substitions should be already applied to the new sub-goals, if any.

improveLit :: Bool -> Prop -> Match (Subst, [Prop])

improveEq :: Bool -> Ctxt -> Prop -> Match (Subst, [Prop])

Improvements from equality constraints. Invariant: the substitions should be already applied to the new sub-goals, if any.