Agda.TypeChecking.Level
Documentation
Constructors
ClosedLevel Integer | |
Plus Integer LevelAtom |
Constructors
MetaLevel MetaId Args | |
BlockedLevel Term | |
NeutralLevel Term |
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source
unLevelAtom :: LevelAtom -> TermSource
unLevelView :: MonadTCM tcm => LevelView -> tcm TermSource