Copyright | License : BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | None |
Language | Haskell2010 |
Implements a proof state, some primitive tactics for manipulating proofs, and some high level commands for introducing new theorems, evaluation/checking inside the proof system, etc.
Documentation
data ProofState Source #
PS | |
|
envAtFocus :: ProofState -> TC Env Source #
goalAtFocus :: ProofState -> TC (Binder Type) Source #
processTactic :: Tactic -> ProofState -> TC (ProofState, String) Source #
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState Source #
doneElaboratingAppPS :: Name -> ProofState -> ProofState Source #
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState Source #
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance) Source #