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
]
data
PlusView
Source
Constructors
ClosedLevel
Integer
Plus
Integer
LevelAtom
data
LevelAtom
Source
Constructors
MetaLevel
MetaId
Args
BlockedLevel
Term
NeutralLevel
Term
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.6.0