Agda.TypeChecking.Primitive
data PrimitiveImpl
data Nat
data Lvl
class PrimType a
class PrimTerm a
class ToTerm a
buildList
type FromTermFunction a
class FromTerm a
redBind
redReturn
fromReducedTerm
fromLiteral
primTrustMe
primQNameType
primQNameDefinition
primDataConstructors
mkPrimLevelZero
mkPrimLevelSuc
mkPrimLevelMax
mkPrimFun1TCM
mkPrimFun1
mkPrimFun2
mkPrimFun4
(-->)
(.-->)
(..-->)
garr
gpi
hPi
nPi
varM
gApply
(<@>)
(<#>)
list
io
el
tset
tSetOmega
tSizeUniv
argN
domN
argH
domH
type Op a
type Fun a
type Rel a
type Pred a
primitiveFunctions
lookupPrimitiveFunction
lookupPrimitiveFunctionQ