Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
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
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
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
)
Source
builtinLevelKit
::
MonadTCM
tcm => tcm (
Maybe
LevelKit
)
Source
requireLevels
::
TCM
LevelKit
Source
Raises an error if no level kit is available.
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.1