ReflectionNames.agda

module ReflectionNames where

postulate Name : Set
{-# BUILTIN QNAME Name #-}

data Bool : Set where
  false : Bool
  true : Bool
{-# BUILTIN BOOL Bool #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE true #-}

postulate String : Set
{-# BUILTIN STRING String #-}

primitive
  primQNameEquality : Name → Name → Bool
  primQNameLess : Name → Name → Bool
  primShowQName : Name → String

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

nameOfNat : Name
nameOfNat = quote Nat

nameOfBool : Name
nameOfBool = quote Bool

isNat : Name → Bool
isNat (quote Nat) = true
isNat _ = false