Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.Monad.Builtin
Contents
The names of built-in things
Synopsis
getBuiltinThings
::
MonadTCM
tcm => tcm (
BuiltinThings
PrimFun
)
setBuiltinThings
::
MonadTCM
tcm =>
BuiltinThings
PrimFun
-> tcm
()
bindBuiltinName
::
MonadTCM
tcm =>
String
->
Term
-> tcm
()
bindPrimitive
::
MonadTCM
tcm =>
String
->
PrimFun
-> tcm
()
getBuiltin
::
MonadTCM
tcm =>
String
-> tcm
Term
getBuiltin'
::
MonadTCM
tcm =>
String
-> tcm (
Maybe
Term
)
getPrimitive
::
MonadTCM
tcm =>
String
-> tcm
PrimFun
primFloat
::
MonadTCM
tcm => tcm
Term
primChar
::
MonadTCM
tcm => tcm
Term
primString
::
MonadTCM
tcm => tcm
Term
primBool
::
MonadTCM
tcm => tcm
Term
primTrue
::
MonadTCM
tcm => tcm
Term
primFalse
::
MonadTCM
tcm => tcm
Term
primList
::
MonadTCM
tcm => tcm
Term
primNil
::
MonadTCM
tcm => tcm
Term
primCons
::
MonadTCM
tcm => tcm
Term
primIO
::
MonadTCM
tcm => tcm
Term
primNat
::
MonadTCM
tcm => tcm
Term
primSuc
::
MonadTCM
tcm => tcm
Term
primZero
::
MonadTCM
tcm => tcm
Term
primNatPlus
::
MonadTCM
tcm => tcm
Term
primNatMinus
::
MonadTCM
tcm => tcm
Term
primNatTimes
::
MonadTCM
tcm => tcm
Term
primNatDivSucAux
::
MonadTCM
tcm => tcm
Term
primNatModSucAux
::
MonadTCM
tcm => tcm
Term
primNatEquality
::
MonadTCM
tcm => tcm
Term
primNatLess
::
MonadTCM
tcm => tcm
Term
primSize
::
MonadTCM
tcm => tcm
Term
primSizeSuc
::
MonadTCM
tcm => tcm
Term
primSizeInf
::
MonadTCM
tcm => tcm
Term
primEquality
::
MonadTCM
tcm => tcm
Term
primRefl
::
MonadTCM
tcm => tcm
Term
primLevel
::
MonadTCM
tcm => tcm
Term
primLevelZero
::
MonadTCM
tcm => tcm
Term
primLevelSuc
::
MonadTCM
tcm => tcm
Term
primLevelMax
::
MonadTCM
tcm => tcm
Term
primInteger
::
MonadTCM
tcm => tcm
Term
builtinTypes
:: [
String
]
Documentation
getBuiltinThings
::
MonadTCM
tcm => tcm (
BuiltinThings
PrimFun
)
Source
setBuiltinThings
::
MonadTCM
tcm =>
BuiltinThings
PrimFun
-> tcm
()
Source
bindBuiltinName
::
MonadTCM
tcm =>
String
->
Term
-> tcm
()
Source
bindPrimitive
::
MonadTCM
tcm =>
String
->
PrimFun
-> tcm
()
Source
getBuiltin
::
MonadTCM
tcm =>
String
-> tcm
Term
Source
getBuiltin'
::
MonadTCM
tcm =>
String
-> tcm (
Maybe
Term
)
Source
getPrimitive
::
MonadTCM
tcm =>
String
-> tcm
PrimFun
Source
The names of built-in things
primFloat
::
MonadTCM
tcm => tcm
Term
Source
primChar
::
MonadTCM
tcm => tcm
Term
Source
primString
::
MonadTCM
tcm => tcm
Term
Source
primBool
::
MonadTCM
tcm => tcm
Term
Source
primTrue
::
MonadTCM
tcm => tcm
Term
Source
primFalse
::
MonadTCM
tcm => tcm
Term
Source
primList
::
MonadTCM
tcm => tcm
Term
Source
primNil
::
MonadTCM
tcm => tcm
Term
Source
primCons
::
MonadTCM
tcm => tcm
Term
Source
primIO
::
MonadTCM
tcm => tcm
Term
Source
primNat
::
MonadTCM
tcm => tcm
Term
Source
primSuc
::
MonadTCM
tcm => tcm
Term
Source
primZero
::
MonadTCM
tcm => tcm
Term
Source
primNatPlus
::
MonadTCM
tcm => tcm
Term
Source
primNatMinus
::
MonadTCM
tcm => tcm
Term
Source
primNatTimes
::
MonadTCM
tcm => tcm
Term
Source
primNatDivSucAux
::
MonadTCM
tcm => tcm
Term
Source
primNatModSucAux
::
MonadTCM
tcm => tcm
Term
Source
primNatEquality
::
MonadTCM
tcm => tcm
Term
Source
primNatLess
::
MonadTCM
tcm => tcm
Term
Source
primSize
::
MonadTCM
tcm => tcm
Term
Source
primSizeSuc
::
MonadTCM
tcm => tcm
Term
Source
primSizeInf
::
MonadTCM
tcm => tcm
Term
Source
primEquality
::
MonadTCM
tcm => tcm
Term
Source
primRefl
::
MonadTCM
tcm => tcm
Term
Source
primLevel
::
MonadTCM
tcm => tcm
Term
Source
primLevelZero
::
MonadTCM
tcm => tcm
Term
Source
primLevelSuc
::
MonadTCM
tcm => tcm
Term
Source
primLevelMax
::
MonadTCM
tcm => tcm
Term
Source
primInteger
::
MonadTCM
tcm => tcm
Term
Source
builtinTypes
:: [
String
]
Source
Produced by
Haddock
version 2.6.0