Cryptol.TypeCheck.Solver.Class

Solving class constraints.

Documentation

classStep :: Prop -> Solved

Solve class constraints. If not, then we return Nothing. If solved, then we return Just a list of sub-goals.

solveZeroInst :: Type -> Solved

Solve a Zero constraint by instance, if possible.

solveLogicInst :: Type -> Solved

Solve a Logic constraint by instance, if possible.

solveArithInst :: Type -> Solved

Solve an Arith constraint by instance, if possible.

solveCmpInst :: Type -> Solved

Solve Cmp constraints.

solveSignedCmpInst :: Type -> Solved

Solve SignedCmp constraints.

solveLiteralInst :: Type -> Type -> Solved

Solve Literal constraints.

expandProp :: Prop -> [Prop]

Add propositions that are implied by the given one. The result contains the orignal proposition, and maybe some more.