Agda.TypeChecking.Level
- newtype LevelView = Max [PlusView]
- data PlusView
- data LevelAtom
- data LevelKit = LevelKit {}
- 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
data LevelAtom
Constructors
MetaLevel MetaId Args | |
BlockedLevel Term | |
NeutralLevel Term |
data LevelKit
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)
Raises an error if no level kit is available.
unLevelAtom :: LevelAtom -> Term
unLevelView :: MonadTCM tcm => LevelView -> tcm Term