Documentation
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source
unLevelAtom :: LevelAtom -> TermSource
unLevelView :: MonadTCM tcm => LevelView -> tcm TermSource
levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)Source
builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)Source
unLevelAtom :: LevelAtom -> TermSource
unLevelView :: MonadTCM tcm => LevelView -> tcm TermSource