HERMIT.Shell.Proof

Documentation

externals :: [External]

Externals that get us into the prover shell, or otherwise deal with lemmas.

data ProofCommand

Constructors

RuleToLemma RuleNameString

InteractiveProof LemmaName

ModifyLemma LemmaName (String -> String) (RewriteH CoreExprEquality) (Bool -> Bool)

QueryLemma LemmaName (TransformH CoreExprEquality String)

ShowLemmas (Maybe LemmaName)

DumpLemma LemmaName String String Int

Instances

Extern ProofCommand

Typeable * ProofCommand

type Box ProofCommand = ProofCommand

performProofCommand :: (MonadCatch m, MonadError CLException m, MonadIO m, MonadState CommandLineState m) => ProofCommand -> m ()

data UserProofTechnique

Instances

Extern UserProofTechnique

type Box UserProofTechnique

userProofTechnique :: TransformH CoreExprEquality () -> UserProofTechnique

ppLemmaT :: PrettyPrinter -> TransformH Lemma DocH