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
- 2023-07-29. Fernando Chu and Fernando Chu. Minor reflection fixes (#685).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).