License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Core.ProofTerm

Description

Synopsis

data ProofTerm
data Goal = GD {
- premises :: Env
- goalType :: Binder Term
}
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

data ProofTerm Source #

Instances

Show ProofTerm Source #
Instance details Defined in Idris.Core.ProofTerm Methods showsPrec :: Int -> ProofTerm -> ShowS # show :: ProofTerm -> String # showList :: [ProofTerm] -> ShowS #

data Goal Source #

Constructors

GD
Fields premises :: Env goalType :: Binder Term

mkProofTerm :: Term -> ProofTerm Source #

getProofTerm :: ProofTerm -> Term Source #

resetProofTerm :: ProofTerm -> ProofTerm Source #

updateSolved :: [(Name, Term)] -> 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 :: ProofTerm -> [Name] Source #

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.

updsubst Source #

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 Source #

type RunTactic' a = Context -> Env -> Term -> StateT a TC Term Source #

goal :: Hole -> ProofTerm -> TC Goal Source #

atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm -> StateT a TC (ProofTerm, Bool) Source #