Copyright | License : BSD3 |
---|---|
Maintainer | The Idris Community. |
Safe Haskell | None |
Language | Haskell98 |
Idris.Core.ProofState
Description
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 #
Constructors
PS | |
Fields
|
Instances
envAtFocus :: ProofState -> TC Env Source #
goalAtFocus :: ProofState -> TC (Binder Type) Source #
Constructors
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 #