Check that an expression is a type.

Check that an expression is a type. * If c == CmpEq, the given sort must be the minimal sort. * If c == CmpLeq, the given sort may be any bigger sort.

Check that an expression is a type and infer its (minimal) sort.

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

We track whether a module telescope came from a data declaration because data telescopes cannot contain tactic arguments (because they result in slightly weird behaviour w.r.t. checking parameters of constructors are fully general)

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 the domain of a function type. Used in checkTypedBindings and to typecheck A.Fun cases.

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 whether we check a typed lambda or a Pi. This flag is needed for irrelevance.

After a typed binding has been checked, add the patterns it binds

Check a tactic attribute. Should have type Term → TC ⊤.

Type check a lambda expression. "checkLambda bs e ty" means ( bs -> e) : ty

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, that's it, we are done.
• If NotADatatype a or CannotEliminateWithPattern p a is thrown and type a is blocked on some meta x, reset any changes to the state and pass (the error and) x to the handler.
• If SplitError (UnificationStuck c tel us vs _) is thrown and the unification problem us =?= vs : tel is blocked on some meta x pass x to the handler.
• If another error was thrown or the type a is not blocked, reraise the error.

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.

Picks up record field assignments from modules that export a definition that has the same name as the missing field.

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

checkRecordUpdate cmp ei recexpr fs e t

Preconditions: e = RecUpdate ei recexpr fs and t is reduced.

Check a record where expression, pushing information about the type of the fields obtained from the context into the let-bindings.

Same as appView, but produces correct Hiding when constructing the AppView from a postfix projection.

Remove top layers of scope info of expression and set the scope accordingly in the TCState.

Type check an expression.

Unquote a TCM computation in a given hole.

Run a tactic `tac : Term → TC ⊤` in a hole (second argument) of the type given by the third argument. Runs the continuation if successful.

Check an interaction point without arguments.

Check an underscore without arguments.

Type check a meta variable.

Infer the type of a meta variable. If it is a new one, we create a new meta for its 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.

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

Check arguments whose value we already know.

This function can be used to check user-supplied parameters we have already computed by inference.

Precondition: The type t of the head has enough domains.

Check an argument whose value we already know.

Check a single argument.

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.

Version of checkLetBinding which traces the fact that we're checking each binding in the Call.