Safe Haskell | None |
---|
Documentation
data ProofState Source
PS | |
|
Show ProofState |
envAtFocus :: ProofState -> TC EnvSource
goalAtFocus :: ProofState -> TC (Binder Type)Source
Show Tactic |
processTactic :: Tactic -> ProofState -> TC (ProofState, String)Source
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofStateSource
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofStateSource