HERMIT.Dictionary.Reasoning

Equational Reasoning

externals

type EqualityProof c m

flipEquality

eqLhsIntroR

eqRhsIntroR

birewrite

extensionalityR

getLemmasT

getLemmaByNameT

insertLemmaR

lemmaR

markLemmaUsedR

modifyLemmaR

Lifting transformations over Equality

lhsT

rhsT

bothT

forallVarsT

lhsR

rhsR

bothR

ppEqualityT

proveEqualityT

verifyEqualityT

verifyEqualityLeftToRightT

verifyEqualityCommonTargetT

verifyIsomorphismT

verifyRetractionT

retractionBR

alphaEqualityR

unshadowEqualityR

instantiateDictsR

instantiateEquality

instantiateEqualityVar

instantiateEqualityVarR

discardUniVars