Agda.TypeChecking.Coverage

Type of variables in scPats.

The patterns leading to the currently considered branch of the split tree.

Substitution from scTel to old context. Only needed directly after split on variable: * To update scTarget * To rename other split variables when splitting on multiple variables. scSubst is not `transitive', i.e., does not record the substitution from the original context to scTel over a series of splits. It is freshly computed after each split by computeNeighborhood; also splitResult, which does not split on a variable, should reset it to the identity idS, lest it be applied to scTarget again, leading to Issue 1294.

We need to keep track of the module parameter checkpoints for the clause for the purpose of inferring missing instance clauses.

The type of the rhs, living in context scTel. fixTargetType computes the new scTarget by applying substitution scSubst.

De Bruijn level (counting dot patterns) of argument we split on.

Covering clauses, indexed by constructor/literal these clauses share.