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

Agda.TypeChecking.Level

Synopsis

- newtype LevelView = Max [PlusView]
- data PlusView
  - = ClosedLevel Integer
  - | Plus Integer LevelAtom
- data LevelAtom
  - = MetaLevel MetaId Args
  - | BlockedLevel Term
  - | NeutralLevel Term
- data LevelKit = LevelKit {
  - levelType :: Term
  - levelSuc :: Term -> Term
  - levelMax :: Term -> Term -> Term
  - levelZero :: Term
  - typeName :: QName
  - sucName :: QName
  - maxName :: QName
  - zeroName :: QName
  }
- levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)
- builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)
- requireLevels :: TCM LevelKit
- unLevelAtom :: LevelAtom -> Term
- unLevelView :: MonadTCM tcm => LevelView -> tcm Term
- maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
- maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)
- levelView :: MonadTCM tcm => Term -> tcm LevelView

# Documentation

newtype LevelView

Constructors

Max [PlusView] |

Instances

Show LevelView |

data PlusView

Constructors

ClosedLevel Integer |
Plus Integer LevelAtom |

Instances

Eq PlusView |
Ord PlusView |
Show PlusView |

data LevelAtom

Constructors

MetaLevel MetaId Args |
BlockedLevel Term |
NeutralLevel Term |

Instances

Eq LevelAtom |
Ord LevelAtom |
Show LevelAtom |

data LevelKit

Constructors

LevelKit |

Fields

levelType :: Term
levelSuc :: Term -> Term
levelMax :: Term -> Term -> Term
levelZero :: Term
typeName :: QName
sucName :: QName
maxName :: QName
zeroName :: QName

levelSucFunction :: MonadTCM tcm => tcm (Term -> Term)

builtinLevelKit :: MonadTCM tcm => tcm (Maybe LevelKit)

requireLevels :: TCM LevelKit

Raises an error if no level kit is available.

unLevelAtom :: LevelAtom -> Term

unLevelView :: MonadTCM tcm => LevelView -> tcm Term

maybePrimCon :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)

maybePrimDef :: MonadTCM tcm => TCM Term -> tcm (Maybe QName)

levelView :: MonadTCM tcm => Term -> tcm LevelView