| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Level

Documentation

newtype LevelView | Source

Constructors

Max [PlusView] |

Instances

Show LevelView

data PlusView | Source

Constructors

ClosedLevel Integer |
Plus Integer LevelAtom |

Instances

Eq PlusView
Ord PlusView
Show PlusView

data LevelAtom | Source

Constructors

MetaLevel MetaId Args |
BlockedLevel Term |
NeutralLevel Term |

Instances

Eq LevelAtom
Ord LevelAtom
Show LevelAtom

data LevelKit | Source

Constructors

LevelKit |

levelSuc :: Term -> Term |
levelMax :: Term -> Term -> Term |
levelZero :: Term |
sucName :: QName |
maxName :: QName |
zeroName :: QName |

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

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

unLevelAtom :: LevelAtom -> Term | Source

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

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

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

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

Produced by Haddock version 2.4.2