Names

Content created by Fernando Chu and Fredrik Bakke.

Created on 2023-04-27.
Last modified on 2023-07-29.

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 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 : UU lzero
{-# BUILTIN QNAME Name #-}

primitive
  primQNameEquality : Name → Name → bool
  primQNameLess : Name → Name → bool
  primShowQName : Name → String
  primQNameToWord64s : Name → Word64 × Word64
  primQNameToWord64sInjective :
    ∀ a b → primQNameToWord64s a ＝ primQNameToWord64s b → a ＝ b

Examples

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

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

Recent changes