Agda.Syntax.Builtin

Either a BuiltinId or PrimitiveId, used for some lookups.

The class of types which can be converted to SomeBuiltin.

A builtin name, defined by the BUILTIN pragma.

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{-# BUILTIN TYPE Type #-}

The type of Type would be Type : Level → Setω which is not valid Agda.

Lookup a builtin by the string used in the BUILTIN pragma.

A primitive name, defined by the primitive block.

Lookup a primitive by its identifier.