Documentation

Fields

thname :: Name

 

holes :: [Name]

holes still to be solved

usedns :: [Name]

used names, don't use again

nextname :: Int

name supply, for locally unique names

global_nextname :: Int

a mirror of the global name supply, for generating things like type tags in reflection

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, ([FailContext], [Name]))]

unsolved auto implicits with their holes

psnames :: [Name]

Local names okay to use in proof search

previous :: Maybe ProofState

for undo

context :: Context

 

datatypes :: Ctxt TypeInfo

 

plog :: String

 

unifylog :: Bool

 

done :: Bool

 

recents :: [Name]

 

while_elaborating :: [FailContext]

 

Fields

premises :: Env

 

goalType :: Binder Term