Check that an expression is a type.

Check that an expression is a type without knowing the sort.

Ensure that a (freshly created) function type does not inhabit SizeUniv. Precondition: When noFunctionsIntoSize t tBlame is called, we are in the context of tBlame in order to print it correctly. Not being in context of t should not matter, as we are only checking whether its sort reduces to SizeUniv.

Check that an expression is a type which is equal to a given type.

Type check a (module) telescope. Binds the variables defined by the telescope.

Type check the telescope of a dependent function type. Binds the resurrected variables defined by the telescope. The returned telescope is unmodified (not resurrected).

Flag to control resurrection on domains.

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.

Parametrized by a flag wether we check a typed lambda or a Pi. This flag is needed for irrelevance.

Type check a lambda expression.

Checking a lambda whose domain type has already been checked.

Insert hidden lambda until the hiding info of the domain type matches the expected hiding info. Throws WrongHidingInLambda

checkAbsurdLambda i h e t checks absurd lambda against type t. Precondition: e = AbsurdLam i h

checkExtendedLambda i di qname cs e t check pattern matching lambda. Precondition: e = ExtendedLam i di qname cs

Run a computation.

• If successful, return Nothing.
• If IlltypedPattern p a is thrown and type a is blocked on some meta x return Just x. Note that the returned meta might only exists in the state where the error was thrown, thus, be an invalid MetaId in the current state.
• If another error was thrown or the type a is not blocked, reraise the error.

checkRecordExpression fs e t checks record construction against type t. Precondition e = Rec _ fs.

checkRecordUpdate ei recexpr fs e t Precondition e = RecUpdate ei recexpr fs.

checkArguments' exph r args t0 t k tries checkArguments exph args t0 t. If it succeeds, it continues k with the returned results. If it fails, it registers a postponed typechecking problem and returns the resulting new meta variable.

Checks e := ((_ : t0) args) : t.

Type check an expression.

checkApplication hd args e t checks an application. Precondition: Application hs args = appView e

checkApplication disambiguates constructors (and continues to checkConstructorApplication) and resolves pattern synonyms.

Unquote a TCM computation in a given hole.

Turn a domain-free binding (e.g. lambda) into a domain-full one, by inserting an underscore for the missing type.

Type check a meta variable. If its type is not given, we return its type, or a fresh one, if it is a new meta. If its type is given, we check that the meta has this type, and we return the same type.

Infer the type of a head thing (variable, function symbol, or constructor). We return a function that applies the head to arguments. This is because in case of a constructor we want to drop the parameters.

Check the type of a constructor application. This is easier than a general application since the implicit arguments can be inserted without looking at the arguments to the 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 the evaluated arguments vs, the remaining type t0' (which should be a subtype of t1) and any constraints cs that have to be solved for everything to be well-formed.

Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.

Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

Used to check aliases f = e. Switches off ExpandLast for the checking of top-level application.

Check whether a de Bruijn index is bound by a module telescope.

Infer the type of an expression, and if it is of the form {tel} -> D vs for some datatype D then insert the hidden arguments. Otherwise, leave the type polymorphic.