Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Level

Synopsis

- data LevelKit = LevelKit {
  - lvlType :: Term
  - lvlSuc :: Term -> Term
  - lvlMax :: Term -> Term -> Term
  - lvlZero :: Term
  - typeName :: QName
  - sucName :: QName
  - maxName :: QName
  - zeroName :: QName
  }
- 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 :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level
- levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level
- levelLub :: Level -> Level -> Level
- subLevel :: Integer -> Level -> Maybe Level

# Documentation

data LevelKit Source #

Constructors

LevelKit |

Fields

- lvlType :: Term
- lvlSuc :: Term -> Term
- lvlMax :: Term -> Term -> Term
- lvlZero :: Term
- typeName :: QName
- sucName :: QName
- maxName :: QName
- zeroName :: QName

levelType :: TCM Type Source #

Get the `primLevel` as a `Type`.

levelSucFunction :: TCM (Term -> Term) Source #

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.

unLevel :: HasBuiltins m => Term -> m Term Source #

reallyUnLevelView :: HasBuiltins m => Level -> m Term Source #

unlevelWithKit :: LevelKit -> Level -> Term Source #

unPlusV :: Term -> (Term -> Term) -> PlusLevel -> Term Source #

maybePrimCon :: TCM Term -> TCM (Maybe ConHead) Source #

maybePrimDef :: TCM Term -> TCM (Maybe QName) Source #

levelView :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level Source #

levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m) => Term -> m Level Source #

levelLub :: Level -> Level -> Level Source #

subLevel :: Integer -> Level -> Maybe Level Source #