|
Agda.TypeChecking.Monad.Signature |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Add a constant to the signature. Lifts the definition to top level.
|
|
|
|
|
|
|
|
|
|
|
Add a section to the signature.
|
|
|
Lookup a section. If it doesn't exist that just means that the module
wasn't parameterised.
|
|
|
|
|
|
|
|
|
|
|
Can be called on either a (co)datatype, a record type or a
(co)constructor.
|
|
|
Does the given constructor come from a single-constructor type?
Precondition: The name has to refer to a constructor.
|
|
|
Lookup the definition of a name. The result is a closed thing, all free
variables have been abstracted over.
|
|
|
Look up the polarity of a definition.
|
|
|
|
|
Set the polarity of a definition.
|
|
|
|
|
|
|
Look up the number of free variables of a section. This is equal to the
number of parameters if we're currently inside the section and 0 otherwise.
|
|
|
Compute the number of free variables of a module. This is the sum of
the free variables of its sections.
|
|
|
Compute the number of free variables of a defined name. This is the sum of
the free variables of the sections it's contained in.
|
|
|
Compute the context variables to apply a definition to.
|
|
|
Instantiate a closed definition with the correct part of the current
context.
|
|
|
Give the abstract view of a definition.
|
|
|
Enter abstract mode. Abstract definition in the current module are transparent.
|
|
|
Not in abstract mode. All abstract definitions are opaque.
|
|
|
Ignore abstract mode. All abstract definitions are transparent.
|
|
|
Check whether a name might have to be treated abstractly (either if we're
inAbstractMode or it's not a local name). Returns true for things not
declared abstract as well, but for those makeAbstract will have no effect.
|
|
|
|
|
get type of a constant
|
|
|
get relevance of a constant
|
|
|
The name must be a datatype.
|
|
|
Is it the name of a record projection?
|
|
Produced by Haddock version 2.6.1 |