Agda.TypeChecking.Reduce

Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).

A variant of instantiateFull that only instantiates those meta-variables that satisfy the predicate.

instantiateFull' instantiates metas everywhere (and recursively) but does not reduce.

Is something (an elimination of) a meta variable? Does not perform any reductions.

Reduce a non-primitive definition if it is a copy linking to another def.

Specialized version to put in boot file.

Reduce simple (single clause) definitions.

Unfold a single inlined function.

Apply a defined function to it's arguments, using the original clauses.

Throw pattern violation if blocked or a meta.

Case on whether a term is blocked on a meta (or is a meta). That means it can change its shape when the meta is instantiated.

Throw a pattern violation if the argument is Blocked, otherwise return the value embedded in the NotBlocked.

Run the given computation but turn any errors into blocked computations with the given blocker

Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched. We include reduction of IApply patterns, as `p i0` is akin to matcing on the i0 constructor of interval.