cryptol-2.10.0: Cryptol: The Language of Cryptography
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.TypeCheck.Solver.Improve

Description

Look for opportunity to solve goals by instantiating variables.

Synopsis

Documentation

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

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]) Source #

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

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

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