|
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.
|
|
|
| Methods | | | Instances | |
|
|
|
|
|
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.
|
|
|
|
|
|
|
Eta expand metavariables listening on the current meta.
|
|
|
Eta expand a metavariable.
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
Produced by Haddock version 2.4.2 |