Stringify postulated objects

cite.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.String

_>>_ = primStringAppend
infixl 1 _>>_

postulate ω : ℕ

data Singular : ℕ → Set where
  singular : (n : ℕ) → Singular n
  cite     : ∀{n} → Singular n → Singular n


show : ℕ → String
show zero = "zero"
show (suc n) = "suc(" >> show n >> ")"

stringify : ∀{n} → Singular n → String
stringify {n} (singular n) = show n
stringify {n} (cite x) = "Unknown"

s0 = singular 0 -- "zero"
s5 = singular 5 -- "suc(suc(suc(suc(suc(zero)))))"
sw = singular ω -- show ω
cw = cite sw    -- "Unknown"

-- Agda can't stringify sw since it doesn't know what it is, but the cite
-- constructor allows you to hide this