| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.Shell.Proof
- externals :: [External]
- data ProofCommand
- performProofCommand :: (MonadCatch m, MonadException m, CLMonad m) => ProofCommand -> m ()
- data UserProofTechnique
- userProofTechnique :: TransformH Equality () -> UserProofTechnique
- ppLemmaT :: PrettyPrinter -> LemmaName -> TransformH Lemma DocH
Documentation
externals :: [External] Source
Externals that get us into the prover shell, or otherwise deal with lemmas. TODO: InteractiveProof is the only one that should be here, rest in Reasoning
data ProofCommand Source
Constructors
| InteractiveProof LemmaName | |
| ShowLemmas (Maybe LemmaName) | |
| DumpLemma LemmaName String String Int |
Instances
performProofCommand :: (MonadCatch m, MonadException m, CLMonad m) => ProofCommand -> m () Source
data UserProofTechnique Source
Instances
ppLemmaT :: PrettyPrinter -> LemmaName -> TransformH Lemma DocH Source