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

mlevel :: TCM (Maybe Term)

Get the 'primLevel as a Term, if present.

levelType :: TCM Type

Get the primLevel as a Type.

levelSucFunction :: TCM (Term -> Term)

builtinLevelKit :: TCM (Maybe LevelKit)

requireLevels :: TCM LevelKit

Raises an error if no level kit is available.

unLevel :: Term -> TCM Term

reallyUnLevelView :: MonadTCM tcm => Level -> tcm Term

unlevelWithKit :: LevelKit -> Level -> Term

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

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

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

levelView :: Term -> TCM Level

levelView' :: Term -> ReduceM Level

levelLub :: Level -> Level -> Level