Set the names of definitions to be looked at to the defs in the current mutual block.

Is a def in the list of stuff to be checked?

Remove a def from the list of defs to be looked at.

Extra environment for the occurs check. (Complements FreeEnv.)

The passed modality is the one of the current context.

Check whether a free variable is allowed in the context as specified by the modality.

Occurs check fails if a defined name is not available since it was declared in irrelevant or erased context.

Construct a test whether a de Bruijn index is allowed or needs to be pruned.

Unfold definitions during occurs check? This effectively runs the occurs check on the normal form.

For a path constructor `c : ... -> Path D a b`, we have that e.g. `c es i0` reduces to a. So we have to consider its arguments as flexible when we do not actually unfold.

Leave the strongly rigid position.

Extended occurs check.

When assigning m xs := v, check that m does not occur in v and that the free variables of v are contained in xs.

prune m' vs xs attempts to remove all arguments from vs whose free variables are not contained in xs. If successful, m' is solved by the new, pruned meta variable and we return True else False.

Issue 1147: If any of the meta args vs is matchable, e.g., is a constructor term, we cannot prune, because the offending variables could be removed by reduction for a suitable instantiation of the meta variable.

hasBadRigid xs v = Just True iff one of the rigid variables in v is not in xs. Actually we can only prune if a bad variable is in the head. See issue 458. Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).

hasBadRigid xs v = Nothing means that we cannot prune at all as one of the meta args is matchable. (See issue 1147.)

Check whether a term Def f es is finally stuck. Currently, we give only a crude approximation.

Check whether any of the variables (given as de Bruijn indices) occurs *definitely* in the term in a rigid position. Reduces the term successively to remove variables in dead subterms. This fixes issue 1386.

Collect the *definitely* rigid variables in a monoid. We need to successively reduce the expression to do this.

killArgs [k1,...,kn] X prunes argument i from metavar X if ki==True. Pruning is carried out whenever > 0 arguments can be pruned.

killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t') (ignoring Dom). Let t' = (xs:as) -> b. Invariant: k'i == True iff ki == True and pruning the ith argument from type b is possible without creating unbound variables. t' is type t after pruning all k'i==True.

Instantiate a meta variable with a new one that only takes the arguments which are not pruneable.