cryptol-2.11.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Solve

Description

 
Synopsis

Documentation

proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst Source #

Prove an implication, and return any improvements that we computed. Records errors, if any of the goals couldn't be solved.

proveModuleTopLevel :: InferM () Source #

Try to clean-up any left-over constraints after we've checked everything in a module. Typically these are either trivial things, or constraints on the module's type parameters.