Safe Haskell | None |
---|
- data LevelKit = LevelKit {}
- levelSucFunction :: TCM (Term -> Term)
- builtinLevelKit :: TCM (Maybe LevelKit)
- requireLevels :: TCM LevelKit
- unLevel :: Term -> TCM Term
- reallyUnLevelView :: Level -> TCM Term
- maybePrimCon :: TCM Term -> TCM (Maybe QName)
- maybePrimDef :: TCM Term -> TCM (Maybe QName)
- levelView :: Term -> TCM Level
- levelLub :: Level -> Level -> Level
Documentation
levelSucFunction :: TCM (Term -> Term)Source
requireLevels :: TCM LevelKitSource
Raises an error if no level kit is available.
reallyUnLevelView :: Level -> TCM TermSource