Agda.TypeChecking.Primitive

Primitive functions

data PrimitiveImpl

data Nat

data Lvl

class PrimType a

class PrimTerm a

class ToTerm a

type FromTermFunction a

class FromTerm a

fromReducedTerm

mkPrimLevelZero

The actual primitive functions

type Op a

type Fun a

type Rel a

type Pred a

primitiveFunctions

lookupPrimitiveFunction

lookupPrimitiveFunctionQ