module RewriteQuote where

open import Data.Bool
open import Data.Nat
open import Function

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

infixr 5 _`+_
data Q : Set → Set₁ where
  `0   : Q ℕ
  `s   : Q ℕ → Q ℕ
  _`+_ : Q ℕ → Q ℕ → Q ℕ
  `λ   : {A B : Set} → Q B → Q (A → B)
  lift : (A : Set) (a : A) → Q A
  pair : (m n : ℕ) → Q Bool

postulate

  myQuote : (A : Set) → Q A → Q A → Set
  myQuote0 : myQuote ℕ (lift ℕ 0) `0
  myQuotes : (m : ℕ) → myQuote ℕ (lift ℕ (suc m)) (`s (lift ℕ m))
  myQuote+ : ∀ m p → myQuote ℕ (lift ℕ (m + p)) (lift ℕ m `+ lift ℕ p)
  myComparemm : (m : ℕ)   → myQuote _ (pair m m) (lift _ true)
  myComparemn : (m n : ℕ) → myQuote _ (pair m n) (lift _ false)

{-# BUILTIN REWRITE myQuote #-}
{-# REWRITE myQuote0 #-}
{-# REWRITE myQuotes #-}
{-# REWRITE myQuote+ #-}
{-# REWRITE myComparemm #-}