idris

Safe HaskellNone

Core.ProofState

Documentation

data ProofState Source

Constructors

PS 

Fields

thname :: Name
 
holes :: [Name]
 
usedns :: [Name]
 
nextname :: Int
 
pterm :: Term
 
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
 

Instances

newProof :: Name -> Context -> Type -> ProofStateSource

envAtFocus :: ProofState -> TC EnvSource

goalAtFocus :: ProofState -> TC (Binder Type)Source

data Tactic Source

Constructors

Attack 
Claim Name Raw 
Reorder Name 
Exact Raw 
Fill Raw 
MatchFill Raw 
PrepFill Name [Name] 
CompleteFill 
Regret 
Solve 
StartUnify Name 
EndUnify 
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 
Equiv Raw 
PatVar Name 
PatBind Name 
Focus Name 
Defer Name 
DeferType Name Raw [Name] 
Instance Name 
SetInjective Name 
MoveLast Name 
MatchProblems 
UnifyProblems 
ProofState 
Undo 
QED 

Instances

data Goal Source

Constructors

GD 

Fields

premises :: Env
 
goalType :: Binder Term
 

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

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

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