diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 6f952604cb..4ac81aba39 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -188,6 +188,11 @@ fun _ => do
   | Except.ok env   => setEnv env
   | Except.error ex => logElabException (ElabException.kernel ex)
 
+@[builtinCommandElab «variable»] def elabVariable : CommandElab :=
+fun n => do
+  runIO (IO.println n.val);
+  pure ()
+
 @[builtinCommandElab «resolve_name»] def elabResolveName : CommandElab :=
 fun n => do
   let id := n.getIdAt 1;
diff --git a/library/init/lean/elaborator/term.lean b/library/init/lean/elaborator/term.lean
index 939fa8399e..fbb1ffa223 100644
--- a/library/init/lean/elaborator/term.lean
+++ b/library/init/lean/elaborator/term.lean
@@ -38,5 +38,10 @@ partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax
 def elabTerm (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab (Syntax Expr) :=
 elabTermAux stx expectedType false
 
+@[builtinTermElab «list»] def elabList : TermElab :=
+fun stx _ => do
+  runIO (IO.println stx.val);
+  pure stx.val
+
 end Elab
 end Lean