Idris.Core.ProofTerm

Documentation

data ProofTerm

Instances

Show ProofTerm

Methods

showsPrec :: Int -> ProofTerm -> ShowS

show :: ProofTerm -> String

showList :: [ProofTerm] -> ShowS

data Goal

Constructors

GD

Fields

• premises :: Env
• goalType :: Binder Term

mkProofTerm :: Term -> ProofTerm

getProofTerm :: ProofTerm -> Term

resetProofTerm :: ProofTerm -> ProofTerm

updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

updateSolvedTerm :: [(Name, Term)] -> Term -> Term

Given a list of solved holes, fill out the solutions in a term

updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool)

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 :: ProofTerm -> [Name]

bound_in_term :: Term -> [Name]

refocus :: Hole -> ProofTerm -> ProofTerm

Refocus the proof term zipper on a particular hole, if it exists. If not, return the original proof term.

updsubst

Arguments

:: Eq n

=> n

The id to replace

-> TT n

The replacement term

-> TT n

The term to replace in

-> TT n

As subst, in TT, but takes advantage of knowing not to substitute under Complete applications.

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)