Agda.TypeChecking.Level

Get the primLevel as a Type. Aborts if any of the level BUILTINs is undefined.

Get the primLevel as a Type. Unsafe, crashes if the BUILTIN LEVEL is undefined.

Raises an error if no level kit is available.

Checks whether level kit is fully available.

Given a level l, find the maximum constant n such that l = n + l'

Given a level l, find the biggest constant n such that n <= l

Given a constant n and a level l, find the level l' such that l = n + l' (or Nothing if there is no such level). Operates on levels in canonical form.

Given two levels a and b, try to decompose the first one as a = a' ⊔ b (for the minimal value of a').

A SingleLevel is a Level that cannot be further decomposed as a maximum a ⊔ b.

Return the maximum of the given SingleLevels