Documentation

Fields

thname :: Name

 

holes :: [Name]

holes still to be solved

usedns :: [Name]

used names, don't use again

nextname :: Int

name supply

pterm :: ProofTerm

current proof term

ptype :: Type

original goal

dontunify :: [Name]

explicitly given by programmer, leave it

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

 

notunified :: [(Name, Term)]

 

dotted :: [(Name, [Name])]

dot pattern holes + environment either hole or something in env must turn up in the notunified list during elaboration

solved :: Maybe (Name, Term)

 

problems :: Fails

 

injective :: [Name]

 

deferred :: [Name]

names we'll need to define

instances :: [Name]

instance arguments (for type classes)

autos :: [(Name, [Name])]

unsolved auto implicits with their holes

previous :: Maybe ProofState

for undo

context :: Context

 

plog :: String

 

unifylog :: Bool

 

done :: Bool

 

recents :: [Name]

 

while_elaborating :: [FailContext]

 

Fields

premises :: Env

 

goalType :: Binder Term