Agda-2.4.2: A dependently typed functional programming language and proof assistant

Safe Haskell	None

Agda.TypeChecking.Level

Synopsis

Documentation

data LevelKit Source

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)Source

Get the 'primLevel as a Term, if present.

levelType :: TCM Type Source

Get the primLevel as a Type.

levelSucFunction :: TCM (Term -> Term)Source

builtinLevelKit :: TCM (Maybe LevelKit)Source

requireLevels :: TCM LevelKit Source

Raises an error if no level kit is available.

unLevel :: Term -> TCM Term Source

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

unlevelWithKit :: LevelKit -> Level -> Term Source

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

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

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

levelView :: Term -> TCM Level Source

levelView' :: Term -> ReduceM Level Source

levelLub :: Level -> Level -> Level Source