cryptol-3.0.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe
Language | Haskell2010

Cryptol.TypeCheck.Solver.Improve

Description

Look for opportunity to solve goals by instantiating variables.

Synopsis

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

# 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.

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

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.