Agda-2.6.1.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Level

Synopsis

Documentation

data LevelKit Source #

Constructors

LevelKit 

requireLevels :: HasBuiltins m => m LevelKit Source #

Raises an error if no level kit is available.

haveLevels :: HasBuiltins m => m Bool Source #

Checks whether level kit is fully available.

levelPlusView :: Level -> (Integer, Level) Source #

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

levelLowerBound :: Level -> Integer Source #

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

subLevel :: Integer -> Level -> Maybe Level Source #

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.

levelMaxDiff :: Level -> Level -> Maybe Level Source #

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

data SingleLevel Source #

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

Instances

Instances details
Eq SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Show SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Free SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

Methods

freeVars' :: IsVarSet a c => SingleLevel -> FreeM a c Source #

Subst Term SingleLevel Source # 
Instance details

Defined in Agda.TypeChecking.Level

unSingleLevels :: [SingleLevel] -> Level Source #

Return the maximum of the given SingleLevels