idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.ProofState

Documentation

data ProofState Source

Constructors

PS 

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]
 

Instances

data Goal Source

Constructors

GD 

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

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