idris-0.9.15: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.ProofTerm

Documentation

data ProofTerm Source

Instances

Show ProofTerm 

data Goal Source

Constructors

GD 

Fields

premises :: Env
 
goalType :: Binder Term
 

mkProofTerm :: Term -> ProofTermSource

getProofTerm :: ProofTerm -> TermSource

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

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

bound_in :: ProofTerm -> [Name]Source

bound_in_term :: Term -> [Name]Source

refocus :: Hole -> ProofTerm -> ProofTermSource

type Hole = Maybe NameSource

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

goal :: Hole -> ProofTerm -> TC GoalSource

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