Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Level
Synopsis
newtype LevelView = Max [PlusView]
data PlusView
= ClosedLevel Integer
| Plus Integer LevelAtom
data LevelAtom
= MetaLevel MetaId Args
| BlockedLevel Term
| NeutralLevel Term
data LevelKit = LevelKit {
levelType :: Term
levelSuc :: Term -> Term
levelMax :: Term -> Term -> Term
levelZero :: Term
typeName :: QName
sucName :: QName
maxName :: QName
zeroName :: QName
}
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)
requireLevels :: TCM LevelKit
unLevelAtom :: LevelAtom -> Term
unLevelView :: MonadTCM tcm => LevelView -> tcm Term
maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
levelView :: MonadTCM tcm => Term -> tcm LevelView
Documentation
newtype LevelView Source
Constructors
Max [PlusView]
data PlusView Source
Constructors
ClosedLevel Integer
Plus Integer LevelAtom
data LevelAtom Source
Constructors
MetaLevel MetaId Args
BlockedLevel Term
NeutralLevel Term
data LevelKit Source
Constructors
LevelKit
levelType :: Term
levelSuc :: Term -> Term
levelMax :: Term -> Term -> Term
levelZero :: Term
typeName :: QName
sucName :: QName
maxName :: QName
zeroName :: QName
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source
requireLevels :: TCM LevelKitSource
Raises an error if no level kit is available.
unLevelAtom :: LevelAtom -> TermSource
unLevelView :: MonadTCM tcm => LevelView -> tcm TermSource
maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)Source
maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)Source
levelView :: MonadTCM tcm => Term -> tcm LevelViewSource
Produced by Haddock version 2.6.1