Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Level
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
levelSuc :: Term -> Term
levelMax :: Term -> Term -> Term
levelZero :: Term
sucName :: QName
maxName :: QName
zeroName :: QName
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source
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.0