Agda.TypeChecking.Positivity.Occurrence

Arbitrary occurrence (positive and negative).

Negative occurrence.

Positive occurrence, but not strictly positive.

Strictly positive occurrence.

Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records.

The elements of the sequences, read from left to right, explain how to get to the occurrence. The second sequence includes the main information, and if the first sequence is non-empty, then it includes information about the context of the second sequence.

in the nth argument of a define constant

in the principal argument of built-in ∞

as an argument to a bound variable. The polarity, if given, is the polarity of the argument the occurence is in

as an argument of a metavariable

in the type of a constructor

in a datatype index of a constructor

in an endpoint of a higher constructor

in the nth clause of a defined function

matched against in a clause of a defined function

is an index of an inductive family

in the definition of a constant