--- a/reflection-ex.agda	Fri Mar 15 17:35:46 2019 +0900
+++ b/reflection-ex.agda	Tue Mar 26 18:02:06 2019 +0900
@@ -19,6 +19,10 @@
 isNat (quote ℕ) = true
 isNat _           = false
 
+lemma1 = isNat (quote ℕ)
+lemma10 = isNat (quote isNat)
+--  quote Set is not work
+
 postulate Meta : Set
 {-# BUILTIN AGDAMETA Meta #-}
 
@@ -49,6 +53,9 @@
 {-# BUILTIN AGDALITQNAME  name    #-}
 {-# BUILTIN AGDALITMETA   meta    #-}
 
+lemma11 : ℕ -> Literal 
+lemma11 n = nat n
+
 data Visibility : Set where
   visible hidden instance′ : Visibility
 
@@ -322,6 +329,58 @@
 thm : (a b : ℕ) → plus-to-times (a + b) ≡ a * b
 thm a b = refl
 
+to-term : List ℕ → Term
+to-term [] = con (quote List.[]) []
+to-term (h ∷ t) = con (quote List._∷_)
+                 ( arg (arg-info visible relevant ) (lit (nat h ))
+              ∷  ( arg (arg-info visible relevant ) (to-term t) )
+              ∷ []  )
+      
+varlistArgs : List (Arg Term ) → List ℕ → List ℕ 
+
+varlistPattern : List (Arg Pattern ) → ℕ → List ℕ → List ℕ 
+varlistPattern [] n vars = vars
+varlistPattern (arg i (con c ps) ∷ t) n vars = varlistPattern t n (varlistPattern ps n vars)
+varlistPattern (arg i dot ∷ t) n vars =  varlistPattern t n vars
+varlistPattern (arg i (var s) ∷ t) n vars = varlistPattern t (suc n) vars
+varlistPattern (arg i (lit l) ∷ t) n vars = varlistPattern t n vars
+varlistPattern (arg i (proj f) ∷ t) n vars = varlistPattern t n vars
+varlistPattern (arg i absurd ∷ t) n vars = varlistPattern t n vars
+
+varlist1 : Term → List ℕ → List ℕ 
+varlist1 (var n args ) vars =  ( n  ∷ vars )
+varlist1 (con c args) vars =   varlistArgs args vars
+varlist1 (def f args) vars =  varlistArgs args ( 11 ∷  vars )
+varlist1 (lam v (abs s x)) vars = varlist1 x vars
+varlist1 (pat-lam cs args) vars = varlistArgs args vars
+varlist1 (pi a b) vars =  vars  
+varlist1 (agda-sort s) vars =  vars  
+varlist1 (lit l) vars = vars 
+varlist1 (meta x args) vars =  varlistArgs args vars 
+varlist1 unknown vars =  vars 
+
+varlistArgs [] vars = vars
+varlistArgs (arg i x ∷ rest) vars =
+    varlistArgs rest ( varlist1 x vars )
+
+macro
+    varlist : Term → Term → TC ⊤
+    varlist term hole =
+       unify hole ( to-term ( varlist1 term [] ) )
+
+t0 = varlist ℕ
+t1 = \ x y -> varlist ( varlist1 x y ) 
+t2 = varlist ( \ (x : Term ) (y : List ℕ ) ->  varlist1 x y )  --   is normalized as varlist1 which has no variables
+t3 = varlist ( \ ( x y : ℕ ) ->  (x , y) ) 
+t4 = \{A : Set} -> \ (x  y : A ) ->  varlist (\ (z : A -> A )  -> z y) 
+-- t4' = \{A : Set} -> \ (x  y : A ) ->  varlist (\ z  -> z y)
+t5 = \ (x  y :  ℕ )->  varlist ( x , y )
+
+-- copy_term : Set → Set
+-- copy_term = ?
+
+-- lemma : {A : Set} -> (x y : A) -> (p : A -> A ) -> copy_term ( p x ) ≡  p y
+
 postulate magic : Type → Term
 
 macro
@@ -374,7 +433,7 @@
         ( λ ty → bindTC (declareDef (arg (arg-info visible relevant) id-name) ty )
         ( λ _ → defId id-name) )
 
-lemma1 : ( x : Name  ) → mkId x ≡ mkId' x
-lemma1 x = refl
+lemma2 : ( x : Name  ) → mkId x ≡ mkId' x
+lemma2 x = refl
 
 unquoteDecl id′ = mkId id′