|
Agda.TypeChecking.MetaVars |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Find position of a value in a list.
Used to change metavar argument indices during assignment.
reverse is necessary because we are directly abstracting over the list.
|
|
|
Check whether a meta variable is a place holder for a blocked term.
|
|
|
|
|
|
|
|
|
|
The instantiation should not be an InstV or InstS and the MetaId
should point to something Open or a BlockedConst.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Create a new metavariable, possibly -expanding in the process.
|
|
|
|
|
Create a new value meta without -expanding.
|
|
|
Create a new value meta with specific dependencies.
|
|
|
|
|
|
|
|
|
Create a metavariable of record type. This is actually one metavariable
for each field.
|
|
|
|
|
|
|
Construct a blocked constant if there are constraints.
|
|
|
Auxiliary function to create a postponed type checking problem.
|
|
|
|
|
|
|
Eta expand metavariables listening on the current meta.
|
|
|
Do safe eta-expansions for meta (SingletonRecords,Levels).
|
|
|
Various kinds of metavariables.
| Constructors | Records | Meta variables of record type.
| SingletonRecords | Meta variables of "hereditarily singleton" record type.
| Levels | Meta variables of level type, if type-in-type is activated.
|
|
|
|
|
All possible metavariable kinds.
|
|
|
Eta expand a metavariable, if it is of the specified kind.
Don't do anything if the metavariable is a blocked term.
|
|
|
Eta expand blocking metavariables of record type, and reduce the
blocked thing.
|
|
|
|
|
|
|
Assign to an open metavar.
First check that metavar args are in pattern fragment.
Then do extended occurs check on given thing.
|
|
|
|
|
|
|
Check that arguments to a metavar are in pattern fragment.
Assumes all arguments already in whnf.
Parameters are represented as Vars so checkArgs really
checks that all args are unique Vars and returns the
list of corresponding indices for each arg-- done
to not define equality on Term.
reverse is necessary because we are directly abstracting over this list ids.
|
|
|
Check that the parameters to a meta variable are distinct variables.
Andreas, 2010-09-24: Allow non-linear variables that do not appear in FVs.
|
|
|
|
|
|
Produced by Haddock version 2.6.1 |