HERMIT.Dictionary.Reasoning

Equational Reasoning

externals

type EqualityProof c m

eqLhsIntroR

eqRhsIntroR

birewrite

extensionalityR

getLemmasT

getLemmaByNameT

getObligationNotProvenT

insertLemmaT

insertLemmasT

lemmaBiR

lemmaConsequentR

markLemmaUsedT

markLemmaProvenT

modifyLemmaT

showLemmaT

showLemmasT

ppLemmaT

ppQuantifiedT

ppLCoreTCT

Lifting transformations over Quantified

lhsT

rhsT

bothT

lhsR

rhsR

bothR

verifyQuantifiedT

verifyEquivalentT

verifyOrCreateT

verifyEqualityLeftToRightT

verifyEqualityCommonTargetT

verifyIsomorphismT

verifyRetractionT

retractionBR

unshadowQuantifiedR

instantiateDictsR

instantiateQuantifiedVarR

abstractQuantifiedR

discardUniVars