sort package:Agda
This module contains the rules for Agda's sort system viewed as a pure
type system (pts). The specification of a pts consists of a set of
axioms of the form s1 : s2 specifying when a sort fits in
another sort, and a set of rules of the form (s1,s2,s3)
specifying that a pi type with domain in s1 and codomain in
s2 itself fits into sort s3.
To ensure unique principal types, the axioms and rules of Agda's pts
are given by two partial functions univSort' and
piSort' (see Agda.TypeChecking.Substitute). If these
functions return Nothing, a constraint is added to ensure
that the sort will be computed eventually.
One upgrade over the standard definition of a pts is that in
a rule (s1,s2,s3), in Agda the sort s2 can depend on
a variable of some type in s1. This is needed to support
Agda's universe polymorphism where we can have e.g. a function of type
∀ {ℓ} → Set ℓ.
Compute a
SortKit in an environment that supports failures.
When
optLoadPrimitives is set to
False,
sortKit
is a fallible operation, so for the uses of
sortKit in fallible
contexts (e.g.
TCMT), we report a type error rather than
exploding.
Sorts interaction points based on their ranges.
Reconstruct the sort of a term.
Precondition: given term is a well-sorted type.
Reconstruct the minimal sort of a type (ignoring the sort annotation).
Check whether a list is sorted. O(n).
Assumes that the
Ord instance implements a partial order.
the meta is what we might be blocked on.