4
open import Common.Reflect
5
open import Common.Prelude renaming (Nat to ℕ)
7
data _≡_ {a}{A : Set a}(x : A) : A → Set where
10
test₁ : quoteTerm (λ {A : Set} (x : A) → x)
11
≡ lam hidden (lam visible (var 0 []))
14
test₂ : (λ {A : Set} (x : A) → quoteTerm x) ≡ (λ x → var 0 [])
17
test₃ : quoteTerm (0 + 0) ≡ con (quote zero) []
21
id : (A : Set) → A → A
24
test₄ : quoteTerm (zero ∶ ℕ) ≡ con (quote ℕ.zero) []