Agda.TypeChecking.Level

Documentation

data LevelKit

Constructors

LevelKit

Fields

• lvlType :: Term
• lvlSuc :: Term -> Term
• lvlMax :: Term -> Term -> Term
• lvlZero :: Term
• typeName :: QName
• sucName :: QName
• maxName :: QName
• zeroName :: QName

levelType :: HasBuiltins m => m Type

Get the primLevel as a Type.

isLevelType :: (HasBuiltins m, MonadReduce m) => Type -> m Bool

levelSucFunction :: TCM (Term -> Term)

builtinLevelKit :: HasBuiltins m => m LevelKit

requireLevels :: HasBuiltins m => m LevelKit

Raises an error if no level kit is available.

haveLevels :: HasBuiltins m => m Bool

Checks whether level kit is fully available.

unLevel :: HasBuiltins m => Term -> m Term

reallyUnLevelView :: HasBuiltins m => Level -> m Term

unlevelWithKit :: LevelKit -> Level -> Term

unConstV :: Term -> (Term -> Term) -> Integer -> Term

unPlusV :: (Term -> Term) -> PlusLevel -> Term

maybePrimCon :: TCM Term -> TCM (Maybe ConHead)

maybePrimDef :: TCM Term -> TCM (Maybe QName)

levelView :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level

levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level

levelPlusView :: Level -> (Integer, Level)

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

levelLowerBound :: Level -> Integer

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

subLevel :: Integer -> Level -> Maybe Level

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

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

data SingleLevel

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

Constructors

SingleClosed Integer

SinglePlus PlusLevel

Instances

Eq SingleLevel

Defined in Agda.TypeChecking.Level

Methods

(==) :: SingleLevel -> SingleLevel -> Bool

(/=) :: SingleLevel -> SingleLevel -> Bool

Show SingleLevel

Defined in Agda.TypeChecking.Level

Methods

showsPrec :: Int -> SingleLevel -> ShowS

show :: SingleLevel -> String

showList :: [SingleLevel] -> ShowS

Free SingleLevel

Defined in Agda.TypeChecking.Level

Methods

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

Subst Term SingleLevel

Defined in Agda.TypeChecking.Level

Methods

applySubst :: Substitution' Term -> SingleLevel -> SingleLevel

unSingleLevel :: SingleLevel -> Level

unSingleLevels :: [SingleLevel] -> Level

Return the maximum of the given SingleLevels

levelMaxView :: Level -> NonEmpty SingleLevel

singleLevelView :: Level -> Maybe SingleLevel