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

Safe Haskell | None

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
  }
- 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

data LevelKit

Constructors

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

levelSucFunction :: TCM (Term -> Term)

builtinLevelKit :: TCM (Maybe LevelKit)

requireLevels :: TCM LevelKit

Raises an error if no level kit is available.

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