Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data LevelKit = LevelKit {}
- levelType :: TCM Type
- levelSucFunction :: TCM (Term -> Term)
- builtinLevelKit :: HasBuiltins m => m LevelKit
- requireLevels :: TCM LevelKit
- haveLevels :: TCM Bool
- unLevel :: HasBuiltins m => Term -> m Term
- reallyUnLevelView :: HasBuiltins m => Level -> m Term
- unlevelWithKit :: LevelKit -> Level -> Term
- unPlusV :: Term -> (Term -> Term) -> PlusLevel -> Term
- maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
- maybePrimDef :: TCM Term -> TCM (Maybe QName)
- levelView :: Term -> TCM Level
- levelView' :: Term -> ReduceM Level
- levelLub :: Level -> Level -> Level
- subLevel :: Integer -> Level -> Maybe Level
Documentation
builtinLevelKit :: HasBuiltins m => m LevelKit Source #
requireLevels :: TCM LevelKit Source #
Raises an error if no level kit is available.
haveLevels :: TCM Bool Source #
Checks whether level kit is fully available.
reallyUnLevelView :: HasBuiltins m => Level -> m Term Source #