Names

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2024-02-07.

module reflection.names where
Imports
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.identity-types
open import foundation.unit-type
open import foundation.universe-levels

open import primitives.machine-integers
open import primitives.strings

Idea

The Name-Agda type represents quoted names, i.e. they are an abstract syntactic representation of terms. Agda provides primitive functions to manipulate them, giving them an equality and ordering. A closed term can be converted to a quoted name by means of the quote keyword, e.g. quote bool.

Definition

postulate
  Name-Agda : UU lzero

{-# BUILTIN QNAME Name-Agda #-}

primitive
  primQNameEquality : Name-Agda  Name-Agda  bool
  primQNameLess : Name-Agda  Name-Agda  bool
  primShowQName : Name-Agda  String
  primQNameToWord64s : Name-Agda  Word64 × Word64
  primQNameToWord64sInjective :
    (a b : Name-Agda)  primQNameToWord64s a  primQNameToWord64s b  a  b

Examples

_ : primQNameLess (quote bool) (quote unit)  true
_ = refl

_ : primShowQName (quote bool)  "foundation.booleans.bool"
_ = refl

Recent changes