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