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]
   
• constraint_ns :: String
   

Fields

• premises :: Env
   
• goalType :: Binder Term