Idris.Core.ProofState

Documentation

data ProofState

Constructors

PS

Fields

thname :: Name

holes :: [Name]

usedns :: [Name]

nextname :: Int

pterm :: ProofTerm

ptype :: Type

dontunify :: [Name]

unified :: (Name, [(Name, Term)])

notunified :: [(Name, Term)]

solved :: Maybe (Name, Term)

problems :: Fails

injective :: [Name]

deferred :: [Name]

instances :: [Name]

previous :: Maybe ProofState

context :: Context

plog :: String

unifylog :: Bool

done :: Bool

while_elaborating :: [FailContext]

Instances

Show ProofState

newProof :: Name -> Context -> Type -> ProofState

envAtFocus :: ProofState -> TC Env

goalAtFocus :: ProofState -> TC (Binder Type)

data Tactic

Constructors

Attack

Claim Name Raw

Reorder Name

Exact Raw

Fill Raw

MatchFill Raw

PrepFill Name [Name]

CompleteFill

Regret

Solve

StartUnify Name

EndUnify

UnifyAll

Compute

ComputeLet Name

Simplify

HNF_Compute

EvalIn Raw

CheckIn Raw

Intro (Maybe Name)

IntroTy Raw (Maybe Name)

Forall Name Raw

LetBind Name Raw Raw

ExpandLet Name Term

Rewrite Raw

Induction Raw

CaseTac Raw

Equiv Raw

PatVar Name

PatBind Name

Focus Name

Defer [Name] Name

DeferType Name Raw [Name]

Instance Name

SetInjective Name

MoveLast Name

MatchProblems Bool

UnifyProblems

ProofState

Undo

QED

Instances

Show Tactic

data Goal

Constructors

GD

Fields

premises :: Env

goalType :: Binder Term

processTactic :: Tactic -> ProofState -> TC (ProofState, String)

nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState

doneElaboratingAppPS :: Name -> ProofState -> ProofState

doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState

dropGiven :: Eq a => [a] -> [(a, TT a)] -> [a] -> [(a, TT a)]

keepGiven :: Eq a => [a] -> [(a, TT a)] -> [a] -> [(a, TT a)]