HERMIT.Dictionary.Reasoning
externals
type EqualityProof c m
eqLhsIntroR
eqRhsIntroR
birewrite
extensionalityR
getLemmasT
getLemmaByNameT
insertLemmaT
insertLemmasT
lemmaBiR
lemmaConsequentR
markLemmaUsedT
markLemmaProvenT
modifyLemmaT
showLemmaT
showLemmasT
ppLemmaT
ppClauseT
ppLCoreTCT
Clause
lhsT
rhsT
bothT
lhsR
rhsR
bothR
verifyClauseT
lemmaR
quantIdentitiesR
verifyOrCreateT
verifyEqualityLeftToRightT
verifyEqualityCommonTargetT
verifyIsomorphismT
verifyRetractionT
reflexivityR
simplifyClauseR
retractionBR
unshadowClauseR
instantiateDictsR
instantiateClauseVarR
abstractClauseR
($$)
($$$)
(==>)
(-->)
(===)
(/\)
(\/)
class ToCoreExpr a
newLemma