|
Agda.TypeChecking.Rules.Term |
|
|
|
|
|
Synopsis |
|
|
|
|
Types
|
|
|
Check that an expression is a type.
|
|
|
Check that an expression is a type without knowing the sort.
|
|
|
Force a type to be a Pi. Instantiates if necessary. The Hiding is only
used when instantiating a meta variable.
|
|
Telescopes
|
|
|
Type check a telescope. Binds the variables defined by the telescope.
|
|
|
Check a typed binding and extends the context with the bound variables.
The telescope passed to the continuation is valid in the original context.
|
|
|
|
Literal
|
|
|
|
|
|
Terms
|
|
|
|
|
Type check an expression.
|
|
|
Infer the type of a head thing (variable, function symbol, or constructor)
|
|
|
|
|
checkHeadApplication e t hd args checks that e has type t,
assuming that e has the form hd args. The corresponding
type-checked term is returned.
If the head term hd is a coinductive constructor, then a
top-level definition fresh tel = hd args (where the clause is
delayed) is added, where tel corresponds to the current
telescope. The returned term is fresh tel.
Precondition: The head hd has to be unambiguous, and there should
not be any need to insert hidden lambdas.
|
|
|
|
|
|
|
|
Check a list of arguments: checkArgs args t0 t1 checks that
t0 = Delta -> t0' and args : Delta. Inserts hidden arguments to
make this happen. Returns t0' and any constraints that have to be
solve for everything to be well-formed.
TODO: doesn't do proper blocking of terms
|
|
|
Check that a list of arguments fits a telescope.
|
|
|
Infer the type of an expression. Implemented by checking agains a meta
variable.
|
|
Let bindings
|
|
|
|
|
|
Produced by Haddock version 2.6.0 |