idris-0.9.15.1: Functional Programming Language with Dependent Types

Safe Haskell	None

Idris.Core.ProofTerm

Documentation

data ProofTerm Source

Instances

data Goal Source

Constructors

GD
Fields premises :: Env goalType :: Binder Term

mkProofTerm :: Term -> ProofTerm Source

getProofTerm :: ProofTerm -> Term Source

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

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

bound_in :: ProofTerm -> [Name]Source

bound_in_term :: Term -> [Name]Source

refocus :: Hole -> ProofTerm -> ProofTerm Source

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