| Copyright | License : BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell98 |
Idris.Core.ProofTerm
Description
- data ProofTerm
- data Goal = GD {}
- mkProofTerm :: Term -> ProofTerm
- getProofTerm :: ProofTerm -> Term
- resetProofTerm :: ProofTerm -> ProofTerm
- updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm
- updateSolvedTerm :: [(Name, Term)] -> Term -> Term
- updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)
- bound_in :: ProofTerm -> [Name]
- bound_in_term :: Term -> [Name]
- refocus :: Hole -> ProofTerm -> ProofTerm
- updsubst :: Eq n => n -> TT n -> TT n -> TT n
- type Hole = Maybe Name
- type RunTactic' a = Context -> Env -> Term -> StateT a TC Term
- goal :: Hole -> ProofTerm -> TC Goal
- atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm -> StateT a TC (ProofTerm, Bool)
Documentation
mkProofTerm :: Term -> ProofTerm Source #
getProofTerm :: ProofTerm -> Term Source #
resetProofTerm :: ProofTerm -> ProofTerm Source #
updateSolvedTerm :: [(Name, Term)] -> Term -> Term Source #
Given a list of solved holes, fill out the solutions in a term
updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool) Source #
Given a list of solved holes, fill out the solutions in a term. Return whether updates were performed, to facilitate sharing when there are no updates.
bound_in_term :: Term -> [Name] Source #
refocus :: Hole -> ProofTerm -> ProofTerm Source #
Refocus the proof term zipper on a particular hole, if it exists. If not, return the original proof term.