From 9f08156a732fb24456932781b3f6dd48b7aea1d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Jan 2014 11:03:35 -0800
Subject: [PATCH] feat(frontends/lean/parser): combine Echo and Show commands
 into the 'print' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/lean/even.lean                |  4 +--
 examples/lean/ex1.lean                 |  6 ++--
 examples/lean/ex2.lean                 |  4 +--
 examples/lean/ex3.lean                 |  2 +-
 examples/lean/ex5.lean                 |  4 +--
 examples/lean/tactic1.lean             |  2 +-
 examples/lean/tactic_in_lua.lean       |  4 +--
 src/frontends/lean/parser_cmds.cpp     | 46 +++++++++++-------------
 src/frontends/lean/parser_imp.h        |  3 +-
 src/tests/frontends/lean/parser.cpp    | 14 ++++----
 tests/lean/alias1.lean                 |  2 +-
 tests/lean/alias2.lean                 | 12 +++----
 tests/lean/apply_tac1.lean             |  2 +-
 tests/lean/arith1.lean                 | 12 +++----
 tests/lean/arith2.lean                 | 18 +++++-----
 tests/lean/arith3.lean                 |  4 +--
 tests/lean/arith6.lean                 |  4 +--
 tests/lean/arith7.lean                 |  6 ++--
 tests/lean/arrow.lean                  |  8 ++---
 tests/lean/bad10.lean                  |  2 +-
 tests/lean/bad2.lean                   |  2 +-
 tests/lean/bad5.lean                   |  2 +-
 tests/lean/bad7.lean                   |  2 +-
 tests/lean/cast2.lean                  |  4 +--
 tests/lean/coercion1.lean              |  2 +-
 tests/lean/coercion2.lean              | 24 ++++++-------
 tests/lean/compact_def.lean            |  2 +-
 tests/lean/disj1.lean                  |  2 +-
 tests/lean/elab2.lean                  |  5 ++-
 tests/lean/elab3.lean                  |  2 +-
 tests/lean/elab4.lean                  |  2 +-
 tests/lean/elab5.lean                  |  2 +-
 tests/lean/elab7.lean                  |  4 +--
 tests/lean/errmsg1.lean                |  2 +-
 tests/lean/ex1.lean                    |  2 +-
 tests/lean/ex2.lean                    | 14 ++++----
 tests/lean/ex3.lean                    |  2 +-
 tests/lean/exists1.lean                |  2 +-
 tests/lean/exists2.lean                |  2 +-
 tests/lean/exists4.lean                |  2 +-
 tests/lean/exists5.lean                |  2 +-
 tests/lean/exists7.lean                |  2 +-
 tests/lean/exit.lean                   |  2 +-
 tests/lean/ho.lean                     |  2 +-
 tests/lean/implicit1.lean              | 20 +++++------
 tests/lean/implicit3.lean              |  6 ++--
 tests/lean/implicit6.lean              | 12 +++----
 tests/lean/interactive/t10.lean        |  2 +-
 tests/lean/interactive/t12.lean        |  2 +-
 tests/lean/interactive/t13.lean        |  2 +-
 tests/lean/interactive/t2.lean         |  2 +-
 tests/lean/interactive/t3.lean         |  2 +-
 tests/lean/interactive/t4.lean         |  2 +-
 tests/lean/interactive/t5.lean         |  2 +-
 tests/lean/let1.lean                   |  8 ++---
 tests/lean/let2.lean                   |  2 +-
 tests/lean/let3.lean                   |  2 +-
 tests/lean/let4.lean                   |  8 ++---
 tests/lean/lua17.lean                  |  6 ++--
 tests/lean/lua18.lean                  |  8 ++---
 tests/lean/lua5.lean                   |  2 +-
 tests/lean/lua9.lean                   |  2 +-
 tests/lean/norm_tac.lean               |  2 +-
 tests/lean/overload1.lean              |  8 ++---
 tests/lean/overload2.lean              | 10 +++---
 tests/lean/overload2.lean.expected.out |  8 ++---
 tests/lean/pr1.lean                    |  2 +-
 tests/lean/push.lean                   |  2 +-
 tests/lean/scope.lean                  |  2 +-
 tests/lean/showenv.l                   |  4 +--
 tests/lean/single.lean                 |  2 +-
 tests/lean/subst.lean                  |  2 +-
 tests/lean/subst2.lean                 |  2 +-
 tests/lean/subst3.lean                 |  2 +-
 tests/lean/tactic1.lean                |  2 +-
 tests/lean/tactic10.lean               |  2 +-
 tests/lean/tactic13.lean               |  2 +-
 tests/lean/tactic14.lean               |  2 +-
 tests/lean/tactic2.lean                |  6 ++--
 tests/lean/tactic3.lean                |  2 +-
 tests/lean/tactic4.lean                |  2 +-
 tests/lean/tactic5.lean                |  2 +-
 tests/lean/tactic8.lean                |  2 +-
 tests/lean/tactic9.lean                |  2 +-
 tests/lean/tst1.lean                   | 10 +++---
 tests/lean/tst10.lean                  | 26 +++++++-------
 tests/lean/tst11.lean                  |  4 +--
 tests/lean/tst12.lean                  |  4 +--
 tests/lean/tst13.lean                  |  4 +--
 tests/lean/tst14.lean                  |  2 +-
 tests/lean/tst15.lean                  | 10 +++---
 tests/lean/tst16.lean                  | 22 ++++++------
 tests/lean/tst17.lean                  |  2 +-
 tests/lean/tst2.lean                   | 14 ++++----
 tests/lean/tst3.lean                   | 50 +++++++++++++-------------
 tests/lean/tst4.lean                   | 10 +++---
 tests/lean/tst5.lean                   |  8 ++---
 tests/lean/tst6.lean                   | 14 ++++----
 tests/lean/tst7.lean                   |  6 ++--
 tests/lean/tst7.lean.expected.out      |  2 +-
 tests/lean/tst8.lean                   |  4 +--
 tests/lean/unicode.lean                |  8 ++---
 tests/lua/coercion_bug1.lua            |  6 ++--
 tests/lua/front.lua                    |  8 ++---
 104 files changed, 306 insertions(+), 316 deletions(-)

diff --git a/examples/lean/even.lean b/examples/lean/even.lean
index 51cb82cb1..b4a4ba733 100644
--- a/examples/lean/even.lean
+++ b/examples/lean/even.lean
@@ -59,13 +59,13 @@ Theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
 
 -- The following command displays the proof object produced by Lean after
 -- expanding macros, and infering implicit/missing arguments.
-Show Environment 2.
+print Environment 2.
 
 -- By default, Lean does not display implicit arguments.
 -- The following command will force it to display them.
 SetOption pp::implicit true.
 
-Show Environment 2.
+print Environment 2.
 
 -- As an exercise, prove that the sum of two odd numbers is even,
 -- and other similar theorems.
diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean
index d20c2f47e..dff6e1ad5 100644
--- a/examples/lean/ex1.lean
+++ b/examples/lean/ex1.lean
@@ -27,9 +27,9 @@ Theorem T2 : (h a (h a b)) = (h a (h c e)) :=
     CongrH (Refl a) T1
 
 -- Display the last two objects (i.e., theorems) added to the environment
-Show Environment 2
+print Environment 2
 
--- Show implicit arguments
+-- print implicit arguments
 SetOption lean::pp::implicit true
 SetOption pp::width 150
-Show Environment 2
+print Environment 2
diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean
index cafdd0d1c..06a1ea9b2 100644
--- a/examples/lean/ex2.lean
+++ b/examples/lean/ex2.lean
@@ -8,7 +8,7 @@ Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
         in MP P_qr P_q.
 
 SetOption pp::implicit true.
-Show Environment 1.
+print Environment 1.
 
 Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
 := Assume H_abc H_ab H_a,
@@ -16,4 +16,4 @@ Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
             P_bc := (MP H_abc H_a)
         in MP P_bc P_b.
 
-Show Environment 1.
+print Environment 1.
diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean
index e0e0b1846..44f8ef87e 100644
--- a/examples/lean/ex3.lean
+++ b/examples/lean/ex3.lean
@@ -25,4 +25,4 @@ Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a
                        (λ H_a, H_a)
                        (λ H_na, NotImp1 (MT H H_na)).
 
-Show Environment 3.
\ No newline at end of file
+print Environment 3.
\ No newline at end of file
diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean
index 9ca5217ae..20ebb895d 100644
--- a/examples/lean/ex5.lean
+++ b/examples/lean/ex5.lean
@@ -45,7 +45,7 @@ Push
                   let L1 : R w x := Symmetry ! x ! w << H
                   in Transitivity ! x ! w ! x << H << L1))
 
-    Show Environment 1
+    print Environment 1
 Pop
 
 Scope
@@ -70,4 +70,4 @@ Scope
 EndScope
 
 -- Display the last two theorems
-Show Environment 2
\ No newline at end of file
+print Environment 2
\ No newline at end of file
diff --git a/examples/lean/tactic1.lean b/examples/lean/tactic1.lean
index 4597b5735..c873f9dd1 100644
--- a/examples/lean/tactic1.lean
+++ b/examples/lean/tactic1.lean
@@ -24,7 +24,7 @@ Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
               lemma2     : B      := (by auto)
           in (show B /\ A by auto)
 
-Show Environment 1. -- Show proof for the previous theorem
+print Environment 1. -- print proof for the previous theorem
 
 -- When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
 -- Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index 94d0fff92..b6c963ba0 100644
--- a/examples/lean/tactic_in_lua.lean
+++ b/examples/lean/tactic_in_lua.lean
@@ -68,5 +68,5 @@ Theorem T (a b : Bool) : a => b => a /\ b := _.
    (* Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) *)
    done
 
--- Show proof created using our script
-Show Environment 1.
+-- print proof created using our script
+print Environment 1.
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 7dcfc5540..750dcb482 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -32,21 +32,20 @@ static name g_theorem_kwd("Theorem");
 static name g_axiom_kwd("Axiom");
 static name g_universe_kwd("Universe");
 static name g_eval_kwd("Eval");
-static name g_show_kwd("Show");
 static name g_check_kwd("Check");
 static name g_infix_kwd("Infix");
 static name g_infixl_kwd("Infixl");
 static name g_infixr_kwd("Infixr");
 static name g_notation_kwd("Notation");
-static name g_echo_kwd("Echo");
 static name g_set_option_kwd("SetOption");
 static name g_set_opaque_kwd("SetOpaque");
 static name g_options_kwd("Options");
 static name g_env_kwd("Environment");
 static name g_import_kwd("Import");
-static name g_help_kwd("Help");
+static name g_help_kwd("help");
 static name g_coercion_kwd("Coercion");
 static name g_exit_kwd("Exit");
+static name g_print_kwd("print");
 static name g_push_kwd("Push");
 static name g_pop_kwd("Pop");
 static name g_scope_kwd("Scope");
@@ -56,9 +55,9 @@ static name g_namespace_kwd("Namespace");
 static name g_end_namespace_kwd("EndNamespace");
 /** \brief Table/List with all builtin command keywords */
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
-                                        g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
+                                        g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd,
                                         g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
-                                        g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd, g_builtin_kwd,
+                                        g_exit_kwd, g_print_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd, g_builtin_kwd,
                                         g_namespace_kwd, g_end_namespace_kwd};
 // ==========================================
 
@@ -278,12 +277,13 @@ bool parser_imp::is_hidden_object(object const & obj) const {
 }
 
 /** \brief Parse
-    'Show' expr
-    'Show' Environment [num]
-    'Show' Environment all
-    'Show' Options
+    'print' expr
+    'print' Environment [num]
+    'print' Environment all
+    'print' Options
+    'print' [string]
 */
-void parser_imp::parse_show() {
+void parser_imp::parse_print() {
     next();
     if (curr() == scanner::token::CommandId) {
         name opt_id = curr_name();
@@ -337,6 +337,10 @@ void parser_imp::parse_show() {
         } else {
             throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
         }
+    } else if (curr() == scanner::token::StringVal) {
+        std::string msg = curr_string();
+        next();
+        regular(m_io_state) << msg << endl;
     } else {
         expr v = m_elaborator(parse_expr()).first;
         regular(m_io_state) << v << endl;
@@ -469,13 +473,6 @@ void parser_imp::parse_notation_decl() {
     }
 }
 
-/** Parse 'Echo' [string] */
-void parser_imp::parse_echo() {
-    next();
-    std::string msg = check_string_next("invalid echo command, string expected");
-    regular(m_io_state) << msg << endl;
-}
-
 /** Parse 'SetOption' [id] [value] */
 void parser_imp::parse_set_option() {
     next();
@@ -615,12 +612,13 @@ void parser_imp::parse_help() {
                             << "  Import [string]        load the given file" << endl
                             << "  Push                   create a scope (it is just an alias for the command Scope)" << endl
                             << "  Pop                    discard the current scope" << endl
+                            << "  print [expr]           pretty print the given expression" << endl
+                            << "  print Options          print current the set of assigned options" << endl
+                            << "  print [string]         print the given string" << endl
+                            << "  print Environment      print objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
+                            << "  print Environment [num] show the last num objects in the environment" << endl
                             << "  Scope                  create a scope" << endl
                             << "  SetOption [id] [value] set option [id] with value [value]" << endl
-                            << "  Show [expr]            pretty print the given expression" << endl
-                            << "  Show Options           show current the set of assigned options" << endl
-                            << "  Show Environment       show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
-                            << "  Show Environment [num] show the last num objects in the environment" << endl
                             << "  Theorem [id] : [type] := [expr]      define a new theorem" << endl
                             << "  Variable [id] : [type] declare/postulate an element of the given type" << endl
                             << "  Universe [id] [level]  declare a new universe variable that is >= the given level" << endl;
@@ -766,8 +764,8 @@ bool parser_imp::parse_command() {
         parse_axiom();
     } else if (cmd_id == g_eval_kwd) {
         parse_eval();
-    } else if (cmd_id == g_show_kwd) {
-        parse_show();
+    } else if (cmd_id == g_print_kwd) {
+        parse_print();
     } else if (cmd_id == g_check_kwd) {
         parse_check();
     } else if (cmd_id == g_infix_kwd) {
@@ -778,8 +776,6 @@ bool parser_imp::parse_command() {
         parse_op(fixity::Infixr);
     } else if (cmd_id == g_notation_kwd) {
         parse_notation_decl();
-    } else if (cmd_id == g_echo_kwd) {
-        parse_echo();
     } else if (cmd_id == g_set_option_kwd) {
         parse_set_option();
     } else if (cmd_id == g_set_opaque_kwd) {
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index 238abe3eb..7f7e55470 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -394,13 +394,12 @@ private:
     void parse_axiom();
     void parse_eval();
     bool is_hidden_object(object const & obj) const;
-    void parse_show();
+    void parse_print();
     void parse_check();
     unsigned parse_precedence();
     name parse_op_id();
     void parse_op(fixity fx);
     void parse_notation_decl();
-    void parse_echo();
     void parse_set_option();
     void parse_set_opaque();
     optional<std::string> find_lua_file(std::string const & fname);
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
index 128a73191..df7c9c3cf 100644
--- a/src/tests/frontends/lean/parser.cpp
+++ b/src/tests/frontends/lean/parser.cpp
@@ -46,10 +46,10 @@ static void tst1() {
     environment env; io_state ios = init_test_frontend(env);
     parse(env, ios, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
     parse(env, ios, "Eval true && true");
-    parse(env, ios, "Show true && false Eval true && false");
-    parse(env, ios, "Infixl 35 & : and Show true & false & false Eval true & false");
-    parse(env, ios, "Notation 100 if _ then _ fi : implies Show if true then false fi");
-    parse(env, ios, "Show Pi (A : Type), A -> A");
+    parse(env, ios, "print true && false Eval true && false");
+    parse(env, ios, "Infixl 35 & : and print true & false & false Eval true & false");
+    parse(env, ios, "Notation 100 if _ then _ fi : implies print if true then false fi");
+    parse(env, ios, "print Pi (A : Type), A -> A");
     parse(env, ios, "Check Pi (A : Type), A -> A");
 }
 
@@ -82,9 +82,9 @@ static void tst2() {
 
 static void tst3() {
     environment env; io_state ios = init_test_frontend(env);
-    parse(env, ios, "Help");
-    parse(env, ios, "Help Options");
-    parse_error(env, ios, "Help Echo");
+    parse(env, ios, "help");
+    parse(env, ios, "help Options");
+    parse_error(env, ios, "help print");
     check(env, ios, "10.3", mk_real_value(mpq(103, 10)));
     parse(env, ios, "Variable f : Real -> Real. Check f 10.3.");
     parse(env, ios, "Variable g : (Type 1) -> Type. Check g Type");
diff --git a/tests/lean/alias1.lean b/tests/lean/alias1.lean
index 00e8d3390..ee5094e78 100644
--- a/tests/lean/alias1.lean
+++ b/tests/lean/alias1.lean
@@ -1,3 +1,3 @@
 Alias BB : Bool.
 Variable x : BB.
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/alias2.lean b/tests/lean/alias2.lean
index c8c933033..bfbc23453 100644
--- a/tests/lean/alias2.lean
+++ b/tests/lean/alias2.lean
@@ -2,15 +2,15 @@ Push
   Variable Natural : Type.
   Alias ℕℕ : Natural.
   Variable x : Natural.
-  Show Environment 1.
+  print Environment 1.
   SetOption pp::unicode false.
-  Show Environment 1.
+  print Environment 1.
   SetOption pp::unicode true.
-  Show Environment 1.
+  print Environment 1.
   Alias NN : Natural.
-  Show Environment 2.
+  print Environment 2.
   Alias ℕℕℕ : Natural.
-  Show Environment 3.
+  print Environment 3.
   SetOption pp::unicode false.
-  Show Environment 3.
+  print Environment 3.
 Pop
\ No newline at end of file
diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean
index ffddf5796..950b0e68d 100644
--- a/tests/lean/apply_tac1.lean
+++ b/tests/lean/apply_tac1.lean
@@ -22,4 +22,4 @@ Theorem T3 (a : Int) : (P a a) => (f a a).
      Repeat (OrElse (apply Discharge) exact (apply Ax2) (apply Ax1)).
      done.
 
-Show Environment 2.
\ No newline at end of file
+print Environment 2.
\ No newline at end of file
diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean
index a130973b5..aed715373 100644
--- a/tests/lean/arith1.lean
+++ b/tests/lean/arith1.lean
@@ -8,11 +8,11 @@ Check 15 + 10 - 20
 Variable x : Int
 Variable n : Nat
 Variable m : Nat
-Show n + m
-Show n + x + m
+print n + m
+print n + x + m
 SetOption lean::pp::coercion true
-Show n + x + m + 10
-Show x + n + m + 10
-Show n + m + 10 + x
+print n + x + m + 10
+print x + n + m + 10
+print n + m + 10 + x
 SetOption lean::pp::notation false
-Show n + m + 10 + x
+print n + m + 10 + x
diff --git a/tests/lean/arith2.lean b/tests/lean/arith2.lean
index 9a294f5e3..656d50e27 100644
--- a/tests/lean/arith2.lean
+++ b/tests/lean/arith2.lean
@@ -1,16 +1,16 @@
 Import Int.
 Import Real.
-Show 1/2
+print 1/2
 Eval 4/6
-Show 3 div 2
+print 3 div 2
 Variable x : Real
 Variable i : Int
 Variable n : Nat
-Show x + i + 1 + n
+print x + i + 1 + n
 SetOption lean::pp::coercion true
-Show x + i + 1 + n
-Show x * i + x
-Show x - i + x - x >= 0
-Show x < x
-Show x <= x
-Show x > x
\ No newline at end of file
+print x + i + 1 + n
+print x * i + x
+print x - i + x - x >= 0
+print x < x
+print x <= x
+print x > x
\ No newline at end of file
diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean
index 3c1e83c4a..58f055fff 100644
--- a/tests/lean/arith3.lean
+++ b/tests/lean/arith3.lean
@@ -3,8 +3,8 @@ Eval 8 mod 3
 Eval 8 div 4
 Eval 7 div 3
 Eval 7 mod 3
-Show -8 mod 3
+print -8 mod 3
 SetOption lean::pp::notation false
-Show -8 mod 3
+print -8 mod 3
 Eval -8 mod 3
 Eval (-8 div 3)*3 + (-8 mod 3)
\ No newline at end of file
diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean
index bb906197c..7ab9461ce 100644
--- a/tests/lean/arith6.lean
+++ b/tests/lean/arith6.lean
@@ -1,6 +1,6 @@
 Import Int.
 SetOption pp::unicode false
-Show 3 | 6
+print 3 | 6
 Eval 3 | 6
 Eval 3 | 7
 Eval 2 | 6
@@ -10,4 +10,4 @@ Eval x | 3
 Eval 3 | x
 Eval 6 | 3
 SetOption pp::notation false
-Show 3 | x
\ No newline at end of file
+print 3 | x
\ No newline at end of file
diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean
index ae75c0d3a..aa9c1cf17 100644
--- a/tests/lean/arith7.lean
+++ b/tests/lean/arith7.lean
@@ -10,7 +10,7 @@ Eval |x + 1|
 Eval |x + 1| > 0
 Variable y : Int
 Eval |x + y|
-Show |x + y| > x
+print |x + y| > x
 SetOption pp::notation false
-Show |x + y| > x
-Show |x + y| + |y + x| > x
\ No newline at end of file
+print |x + y| > x
+print |x + y| + |y + x| > x
\ No newline at end of file
diff --git a/tests/lean/arrow.lean b/tests/lean/arrow.lean
index 503474295..d575815bc 100644
--- a/tests/lean/arrow.lean
+++ b/tests/lean/arrow.lean
@@ -1,5 +1,5 @@
 Import Int.
-Show (Int -> Int) -> Int
-Show Int -> Int -> Int
-Show Int -> (Int -> Int)
-Show (Int -> Int) -> (Int -> Int) -> Int
+print (Int -> Int) -> Int
+print Int -> Int -> Int
+print Int -> (Int -> Int)
+print (Int -> Int) -> (Int -> Int) -> Int
diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean
index ef57c1376..3a5d58bf1 100644
--- a/tests/lean/bad10.lean
+++ b/tests/lean/bad10.lean
@@ -5,4 +5,4 @@ Variable N : Type.
 Definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
 SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H.
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/bad2.lean b/tests/lean/bad2.lean
index 1d7b7fe3a..d93955ee9 100644
--- a/tests/lean/bad2.lean
+++ b/tests/lean/bad2.lean
@@ -10,4 +10,4 @@ Definition n5 : _ := cons 10 nil
 
 SetOption pp::coercion true
 SetOption pp::implicit true
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/bad5.lean b/tests/lean/bad5.lean
index 0a37ba02b..56ea5fcab 100644
--- a/tests/lean/bad5.lean
+++ b/tests/lean/bad5.lean
@@ -5,4 +5,4 @@ Variable b : Int
 Axiom H1 : a = b
 Axiom H2 : (g a) > 0
 Theorem T1 : (g b) > 0 := SubstP (λ x, (g x) > 0) H2 H1
-Show Environment 2
+print Environment 2
diff --git a/tests/lean/bad7.lean b/tests/lean/bad7.lean
index 10de60a61..472edbf37 100644
--- a/tests/lean/bad7.lean
+++ b/tests/lean/bad7.lean
@@ -3,4 +3,4 @@ Variable f {A : Type} (a b : A) : Bool
 Variable a : Int
 Variable b : Real
 Definition tst : Bool := (fun x y, f x y) a b
-Show Environment 1
+print Environment 1
diff --git a/tests/lean/cast2.lean b/tests/lean/cast2.lean
index 040b1a3bb..91c98d7e2 100644
--- a/tests/lean/cast2.lean
+++ b/tests/lean/cast2.lean
@@ -8,5 +8,5 @@ Variable a : A
 Check DomInj H
 Theorem BeqB' : B = B' := RanInj H a
 SetOption pp::implicit true
-Show DomInj H
-Show RanInj H a
+print DomInj H
+print RanInj H a
diff --git a/tests/lean/coercion1.lean b/tests/lean/coercion1.lean
index 7a0002dbb..778860103 100644
--- a/tests/lean/coercion1.lean
+++ b/tests/lean/coercion1.lean
@@ -2,7 +2,7 @@ Variable T : Type
 Variable R : Type
 Variable f : T -> R
 Coercion f
-Show Environment 2
+print Environment 2
 Variable g : T -> R
 Coercion g
 Variable h : Pi (x : Type), x
diff --git a/tests/lean/coercion2.lean b/tests/lean/coercion2.lean
index 819cd2117..6d7733106 100644
--- a/tests/lean/coercion2.lean
+++ b/tests/lean/coercion2.lean
@@ -4,14 +4,14 @@ Variable t2r : T -> R
 Coercion t2r
 Variable g : R -> R -> R
 Variable a : T
-Show g a a
+print g a a
 Variable b : R
-Show g a b
-Show g b a
+print g a b
+print g b a
 SetOption lean::pp::coercion true
-Show g a a
-Show g a b
-Show g b a
+print g a a
+print g a b
+print g b a
 SetOption lean::pp::coercion false
 Variable S : Type
 Variable s : S
@@ -20,13 +20,13 @@ Variable h : S -> S -> S
 Infixl 10 ++ : g
 Infixl 10 ++ : h
 SetOption lean::pp::notation false
-Show a ++ b ++ a
-Show r ++ s ++ r
+print a ++ b ++ a
+print r ++ s ++ r
 Check a ++ b ++ a
 Check r ++ s ++ r
 SetOption lean::pp::coercion true
-Show a ++ b ++ a
-Show r ++ s ++ r
+print a ++ b ++ a
+print r ++ s ++ r
 SetOption lean::pp::notation true
-Show a ++ b ++ a
-Show r ++ s ++ r
+print a ++ b ++ a
+print r ++ s ++ r
diff --git a/tests/lean/compact_def.lean b/tests/lean/compact_def.lean
index eb7cf2463..5d9b54d82 100644
--- a/tests/lean/compact_def.lean
+++ b/tests/lean/compact_def.lean
@@ -2,4 +2,4 @@ Import specialfn.
 Definition f x y := x + y
 Definition g x y := sin x + y
 Definition h x y := x * sin (x + y)
-Show Environment 3
\ No newline at end of file
+print Environment 3
\ No newline at end of file
diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean
index 38269b38a..0b46b503e 100644
--- a/tests/lean/disj1.lean
+++ b/tests/lean/disj1.lean
@@ -18,4 +18,4 @@ Theorem T2 (a b : Bool) : a \/ b => b \/ a.
     simple_tac.
     done.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/elab2.lean b/tests/lean/elab2.lean
index ba7b9525a..84fc773f3 100644
--- a/tests/lean/elab2.lean
+++ b/tests/lean/elab2.lean
@@ -1,4 +1,3 @@
-
 Variable C : Pi (A B : Type) (H : A = B) (a : A), B
 
 Variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
@@ -8,7 +7,7 @@ Variable R : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A,
 
 Theorem R2 (A A' B B' : Type) (H : (A -> B) = (A' -> B')) (a : A) : B = B' := R _ _ _ _ H a
 
-Show Environment 1
+print Environment 1
 
 Theorem R3 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
     fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1),
@@ -22,4 +21,4 @@ Theorem R5 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1
     fun (A1 A2 B1 B2 : Type) (H : _) (a : _),
         R _ _ _ _ H a
 
-Show Environment 1
+print Environment 1
diff --git a/tests/lean/elab3.lean b/tests/lean/elab3.lean
index 937b776a1..c07795713 100644
--- a/tests/lean/elab3.lean
+++ b/tests/lean/elab3.lean
@@ -9,4 +9,4 @@ Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1
     fun A1 A2 B1 B2 H a,
         R _ _ _ _ H a
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean
index eb5d02b05..1429b12ff 100644
--- a/tests/lean/elab4.lean
+++ b/tests/lean/elab4.lean
@@ -9,4 +9,4 @@ Theorem R2 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1
     fun A1 A2 B1 B2 H a, R H a
 
 SetOption pp::implicit true
-Show Environment 7.
+print Environment 7.
diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean
index aefa79b6c..f699278a4 100644
--- a/tests/lean/elab5.lean
+++ b/tests/lean/elab5.lean
@@ -9,4 +9,4 @@ Theorem R2 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B
     fun A1 A2 B1 B2 H a, R H a
 
 SetOption pp::implicit true
-Show Environment 7.
+print Environment 7.
diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean
index 7708b9417..e77a4029d 100644
--- a/tests/lean/elab7.lean
+++ b/tests/lean/elab7.lean
@@ -16,6 +16,6 @@ Theorem T1 : F1 = F2 := Abst (fun a, (Abst (fun b, H a b)))
 Theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (fun a, (Abst (fun b, H a b)))
 Theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b)))
 Theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b)))
-Show Environment 4
+print Environment 4
 SetOption pp::implicit true
-Show Environment 4
\ No newline at end of file
+print Environment 4
\ No newline at end of file
diff --git a/tests/lean/errmsg1.lean b/tests/lean/errmsg1.lean
index b1502b5c3..4a71e7420 100644
--- a/tests/lean/errmsg1.lean
+++ b/tests/lean/errmsg1.lean
@@ -1,5 +1,5 @@
 Eval fun x, x
-Show fun x, x
+print fun x, x
 
 Check fun x, x
 Theorem T (A : Type) (x : A) : Pi (y : A), A
diff --git a/tests/lean/ex1.lean b/tests/lean/ex1.lean
index 50b374521..72aa9604f 100644
--- a/tests/lean/ex1.lean
+++ b/tests/lean/ex1.lean
@@ -1 +1 @@
-Echo "test"
+print "test"
diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean
index c4556b0a1..8797dcebd 100644
--- a/tests/lean/ex2.lean
+++ b/tests/lean/ex2.lean
@@ -1,18 +1,18 @@
 -- comment
-Show true
+print true
 SetOption lean::pp::notation false
-Show true && false
+print true && false
 SetOption pp::unicode false
-Show true && false
+print true && false
 Variable a : Bool
 Variable a : Bool
 Variable b : Bool
-Show a && b
+print a && b
 Variable A : Type
 Check a && A
-Show Environment 1
-Show Options
+print Environment 1
+print Options
 SetOption lean::p::notation true
 SetOption lean::pp::notation 10
 SetOption lean::pp::notation true
-Show a && b
+print a && b
diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean
index e5dda70db..6304f745b 100644
--- a/tests/lean/ex3.lean
+++ b/tests/lean/ex3.lean
@@ -1,5 +1,5 @@
 Variable myeq : Pi (A : Type), A -> A -> Bool
-Show myeq _ true false
+print myeq _ true false
 Variable T : Type
 Variable a : T
 Check myeq _ true a
diff --git a/tests/lean/exists1.lean b/tests/lean/exists1.lean
index 87bd2072b..1118bc6b4 100644
--- a/tests/lean/exists1.lean
+++ b/tests/lean/exists1.lean
@@ -3,4 +3,4 @@ Variable a : Int
 Variable P : Int -> Int -> Bool
 Axiom H : P a a
 Theorem T : exists x : Int, P a a := ExistsIntro a H.
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/exists2.lean b/tests/lean/exists2.lean
index 28b7ccda1..2b30c73da 100644
--- a/tests/lean/exists2.lean
+++ b/tests/lean/exists2.lean
@@ -15,4 +15,4 @@ Theorem T6 : exists x y : Int, P x y := ExistsIntro _ (ExistsIntro _ H3)
 Theorem T7 : exists x : Int, P (f x x) x := ExistsIntro _ H3
 Theorem T8 : exists x y : Int, P (f x x) y := ExistsIntro _ (ExistsIntro _ H3)
 
-Show Environment 8.
\ No newline at end of file
+print Environment 8.
\ No newline at end of file
diff --git a/tests/lean/exists4.lean b/tests/lean/exists4.lean
index 58bd4bf38..97e2fee94 100644
--- a/tests/lean/exists4.lean
+++ b/tests/lean/exists4.lean
@@ -13,4 +13,4 @@ Theorem T3 : exists x y z : N, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIn
 
 Theorem T4 (H : P a a b) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H))
 
-Show Environment 4
\ No newline at end of file
+print Environment 4
\ No newline at end of file
diff --git a/tests/lean/exists5.lean b/tests/lean/exists5.lean
index 918bb01d0..f3dc7203d 100644
--- a/tests/lean/exists5.lean
+++ b/tests/lean/exists5.lean
@@ -4,4 +4,4 @@ Variables P : N -> N -> N -> Bool
 
 Theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H))
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/exists7.lean b/tests/lean/exists7.lean
index 54e44aa44..59bec1bcb 100644
--- a/tests/lean/exists7.lean
+++ b/tests/lean/exists7.lean
@@ -9,4 +9,4 @@ SetOpaque not     false.
 
 Theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H))
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/exit.lean b/tests/lean/exit.lean
index bf6df28db..90e050aa7 100644
--- a/tests/lean/exit.lean
+++ b/tests/lean/exit.lean
@@ -1,2 +1,2 @@
 Exit
-Show "FAILED"
+print "FAILED"
diff --git a/tests/lean/ho.lean b/tests/lean/ho.lean
index 2de055b75..79e340325 100644
--- a/tests/lean/ho.lean
+++ b/tests/lean/ho.lean
@@ -5,4 +5,4 @@ Variable b : Int
 Axiom H1 : a = b
 Axiom H2 : (g a) > 0
 Theorem T1 : (g b) > 0 := Subst H2 H1
-Show Environment 2
+print Environment 2
diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean
index 59829cf61..91943dde5 100644
--- a/tests/lean/implicit1.lean
+++ b/tests/lean/implicit1.lean
@@ -1,20 +1,20 @@
 Import Int.
 Import Real.
 Variable f : Int -> Int -> Int
-Show forall a, f a a > 0
-Show forall a b, f a b > 0
+print forall a, f a a > 0
+print forall a b, f a b > 0
 Variable g : Int -> Real -> Int
-Show forall a b, g a b > 0
-Show forall a b, g a (f a b) > 0
+print forall a b, g a b > 0
+print forall a b, g a (f a b) > 0
 SetOption pp::coercion true
-Show forall a b, g a (f a b) > 0
-Show fun a, a + 1
-Show fun a b, a + b
-Show fun (a b) (c : Int), a + c + b
+print forall a b, g a (f a b) > 0
+print fun a, a + 1
+print fun a b, a + b
+print fun (a b) (c : Int), a + c + b
 -- The next example shows a limitation of the current elaborator.
 -- The current elaborator resolves overloads before solving the implicit argument constraints.
 -- So, it does not have enough information for deciding which overload to use.
-Show (fun a b, a + b) 10 20.
+print (fun a b, a + b) 10 20.
 Variable x : Int
 -- The following one works because the type of x is used to decide which + should be used
-Show fun a b, a + x + b
\ No newline at end of file
+print fun a b, a + x + b
\ No newline at end of file
diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean
index d4052d23d..99af0e59f 100644
--- a/tests/lean/implicit3.lean
+++ b/tests/lean/implicit3.lean
@@ -1,11 +1,11 @@
 Import Int.
 
-Show 10 = 20
+print 10 = 20
 Variable f : Int -> Int -> Int
 Variable g : Int -> Int -> Int -> Int
 Notation 10 _ ++ _ : f
 Notation 10 _ ++ _ : g
 SetOption pp::implicit true
 SetOption pp::notation false
-Show (10 ++ 20)
-Show (10 ++ 20) 10
+print (10 ++ 20)
+print (10 ++ 20) 10
diff --git a/tests/lean/implicit6.lean b/tests/lean/implicit6.lean
index e03236271..03580073e 100644
--- a/tests/lean/implicit6.lean
+++ b/tests/lean/implicit6.lean
@@ -1,11 +1,11 @@
 Import Int.
 Variable f {A : Type} : A -> A -> A
 Infixl 65 + : f
-Show true + false
-Show 10 + 20
-Show 10 + (- 20)
+print true + false
+print 10 + 20
+print 10 + (- 20)
 SetOption pp::notation false
 SetOption pp::coercion true
-Show true + false
-Show 10 + 20
-Show 10 + (- 20)
+print true + false
+print 10 + 20
+print 10 + (- 20)
diff --git a/tests/lean/interactive/t10.lean b/tests/lean/interactive/t10.lean
index 4d0c578cd..c4c7014cd 100644
--- a/tests/lean/interactive/t10.lean
+++ b/tests/lean/interactive/t10.lean
@@ -12,4 +12,4 @@ Theorem T2 (A B : Bool) : A /\ B => B /\ A :=
    simple2_tac. done.
    simple_tac. done.
 
-Echo "echo command after failure"
\ No newline at end of file
+print "echo command after failure"
\ No newline at end of file
diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean
index 3c07928e4..7aaf302d1 100644
--- a/tests/lean/interactive/t12.lean
+++ b/tests/lean/interactive/t12.lean
@@ -10,7 +10,7 @@ Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
               lemma2     : B      := (by auto)
           in (show B /\ A by auto)
 
-Show Environment 1. -- Show proof for the previous theorem
+print Environment 1. -- print proof for the previous theorem
 
 Theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
      fun assumption : A /\ B,
diff --git a/tests/lean/interactive/t13.lean b/tests/lean/interactive/t13.lean
index 96f3a7bbb..9a2640fbe 100644
--- a/tests/lean/interactive/t13.lean
+++ b/tests/lean/interactive/t13.lean
@@ -9,4 +9,4 @@ Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
               lemma2 := (show B by auto)
           in (show B /\ A by auto)
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean
index 6f9b751d9..f07ff5723 100644
--- a/tests/lean/interactive/t2.lean
+++ b/tests/lean/interactive/t2.lean
@@ -6,4 +6,4 @@ foo.
 abort.
 
 Variables a b : Bool.
-Show Environment 2.
+print Environment 2.
diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
index ec9edaf65..2e61398c6 100644
--- a/tests/lean/interactive/t3.lean
+++ b/tests/lean/interactive/t3.lean
@@ -8,4 +8,4 @@ back.
 exact.
 done.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/interactive/t4.lean b/tests/lean/interactive/t4.lean
index 9214a17c0..46f967abb 100644
--- a/tests/lean/interactive/t4.lean
+++ b/tests/lean/interactive/t4.lean
@@ -1,2 +1,2 @@
 Theorem (a : Bool) : a.
-Echo "done".
\ No newline at end of file
+print "done".
\ No newline at end of file
diff --git a/tests/lean/interactive/t5.lean b/tests/lean/interactive/t5.lean
index 961ac4778..309c224df 100644
--- a/tests/lean/interactive/t5.lean
+++ b/tests/lean/interactive/t5.lean
@@ -5,4 +5,4 @@ Theorem T (a : Bool) : a.
     apply magic.
     done.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean
index 492b0d6d2..5e96f2f12 100644
--- a/tests/lean/let1.lean
+++ b/tests/lean/let1.lean
@@ -1,12 +1,10 @@
 Import Int.
 
-Show let a : Nat := 10, b : Nat := 20, c : Nat := 30, d : Nat := 10 in a + b + c + d
-Show let a : Nat := 1000000000000000000, b : Nat := 20000000000000000000, c : Nat := 3000000000000000000, d : Nat := 4000000000000000000 in a + b + c + d
+print let a : Nat := 10, b : Nat := 20, c : Nat := 30, d : Nat := 10 in a + b + c + d
+print let a : Nat := 1000000000000000000, b : Nat := 20000000000000000000, c : Nat := 3000000000000000000, d : Nat := 4000000000000000000 in a + b + c + d
 Check let a : Nat := 10 in a + 1
 Eval let a : Nat := 20 in a + 10
 Eval let a := 20 in a + 10
 Check let a : Int := 20 in a + 10
 SetOption pp::coercion true
-Show let a : Int := 20 in a + 10
-
-
+print let a : Int := 20 in a + 10
diff --git a/tests/lean/let2.lean b/tests/lean/let2.lean
index 2342e9ae8..aae077c71 100644
--- a/tests/lean/let2.lean
+++ b/tests/lean/let2.lean
@@ -7,4 +7,4 @@ Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
             P_q  : q       := MP P_pq H_p
         in MP P_qr P_q))
 
-Show Environment 1
\ No newline at end of file
+print Environment 1
\ No newline at end of file
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index a439fa95d..938d4b44c 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -4,6 +4,6 @@ Variable magic : Pi (H : Bool), H
 
 SetOption pp::notation false
 SetOption pp::coercion true
-Show let a : Int   := 1,
+print let a : Int   := 1,
          H : a > 0 := magic (a > 0)
      in H
\ No newline at end of file
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 0b63fb051..7d203ef2a 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,6 +1,6 @@
 Import Int.
 
-Show
+print
 let b := true,
     a : Int := b
 in a
@@ -14,7 +14,7 @@ let a  := 10,
     v2 := v1
 in v2
 
-Show
+print
 let a  := 10,
     v1 : vector Bool a := const a true,
     v2 : vector Bool a := v1
@@ -43,10 +43,8 @@ in v2
 
 SetOption pp::coercion true
 
-Show
+print
 let a  := 10,
     v1 : vector Bool a := const a true,
     v2 : vector Int  a := v1
 in v2
-
-
diff --git a/tests/lean/lua17.lean b/tests/lean/lua17.lean
index c5c0348f8..b90c2b220 100644
--- a/tests/lean/lua17.lean
+++ b/tests/lean/lua17.lean
@@ -1,6 +1,6 @@
 Import Int.
 Variables a b : Int
-Show Options
+print Options
 (*
   local ios = io_state()
 
@@ -10,5 +10,5 @@ Show Options
   print(parse_lean("fun x, a + x"))
   print(get_options())
 *)
-Show Options
-Show Environment 2
\ No newline at end of file
+print Options
+print Environment 2
\ No newline at end of file
diff --git a/tests/lean/lua18.lean b/tests/lean/lua18.lean
index 675a868dc..05d1cb149 100644
--- a/tests/lean/lua18.lean
+++ b/tests/lean/lua18.lean
@@ -18,8 +18,8 @@ macro("Sum", { macro_arg.Exprs },
       end)
 *)
 
-Show (MyMacro 10, 20) + 20
-Show (Sum)
-Show Sum 10 20 30 40
-Show fun x, Sum x 10 x 20
+print (MyMacro 10, 20) + 20
+print (Sum)
+print Sum 10 20 30 40
+print fun x, Sum x 10 x 20
 Eval (fun x, Sum x 10 x 20) 100
diff --git a/tests/lean/lua5.lean b/tests/lean/lua5.lean
index fa8a9183c..569e9b12f 100644
--- a/tests/lean/lua5.lean
+++ b/tests/lean/lua5.lean
@@ -11,5 +11,5 @@ for i = 1, N do
 end
 *)
 
-Show Environment 101
+print Environment 101
 Check x + y_1 + y_2
\ No newline at end of file
diff --git a/tests/lean/lua9.lean b/tests/lean/lua9.lean
index e800ad12d..d383d9233 100644
--- a/tests/lean/lua9.lean
+++ b/tests/lean/lua9.lean
@@ -33,6 +33,6 @@ Variable x : Bool
  env:add_definition("sum1", s)
 *)
 
-Show Environment 1
+print Environment 1
 Eval sum1
 Variable y : Bool
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index 7d27b2d04..3c3ef6433 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -7,7 +7,7 @@ Variable vector (A : Type) (sz : Nat) : Type
 Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 Variable V1 : vector Int 10
 Definition D := read V1 1 (by trivial)
-Show Environment 1
+print Environment 1
 Variable b : Bool
 Definition a := b
 Theorem T : b => a := (by (* imp_tac() .. normalize_tac() .. assumption_tac() *))
diff --git a/tests/lean/overload1.lean b/tests/lean/overload1.lean
index 993d22558..229d59a65 100644
--- a/tests/lean/overload1.lean
+++ b/tests/lean/overload1.lean
@@ -3,10 +3,10 @@ Variable f : Bool -> Bool -> Bool
 Variable g : N -> N -> N
 Infixl 10 ++ : f
 Infixl 10 ++ : g
-Show true ++ false ++ true
+print true ++ false ++ true
 SetOption lean::pp::notation false
-Show true ++ false ++ true
+print true ++ false ++ true
 Variable a : N
 Variable b : N
-Show a ++ b ++ a
-Show true ++ false ++ false
\ No newline at end of file
+print a ++ b ++ a
+print true ++ false ++ false
\ No newline at end of file
diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean
index dc377d581..da6cf5dcc 100644
--- a/tests/lean/overload2.lean
+++ b/tests/lean/overload2.lean
@@ -1,6 +1,6 @@
 Import Int
 Import Real
-Show 1 + true
+print 1 + true
 Variable R : Type
 Variable T : Type
 Variable r2t : R -> T
@@ -12,10 +12,10 @@ Variable a : T
 Variable b : R
 SetOption lean::pp::coercion true
 SetOption lean::pp::notation false
-Show f a b
-Show f b a
+print f a b
+print f b a
 Variable g : R -> T -> R
 Infix 10 ++ : f
 Infix 10 ++ : g
-Show a ++ b
-Show b ++ a
+print a ++ b
+print b ++ a
diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out
index 9694b8363..9d1c2e4c0 100644
--- a/tests/lean/overload2.lean.expected.out
+++ b/tests/lean/overload2.lean.expected.out
@@ -4,25 +4,25 @@
   Imported 'Real'
 Failed to solve
  ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add)
-    (line: 3: pos: 9) Overloading at
+    (line: 3: pos: 10) Overloading at
         (Real::add | Int::add | Nat::add) 1 ⊤
     Failed to solve
      ⊢ Bool ≺ ℕ
-        (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of
+        (line: 3: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
             Nat::add
         with arguments:
             1
             ⊤
     Failed to solve
      ⊢ Bool ≺ ℤ
-        (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of
+        (line: 3: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
             Int::add
         with arguments:
             1
             ⊤
     Failed to solve
      ⊢ Bool ≺ ℝ
-        (line: 3: pos: 9) Type of argument 2 must be convertible to the expected type in the application of
+        (line: 3: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
             Real::add
         with arguments:
             1
diff --git a/tests/lean/pr1.lean b/tests/lean/pr1.lean
index 3cb6f8ffa..2f612f343 100644
--- a/tests/lean/pr1.lean
+++ b/tests/lean/pr1.lean
@@ -3,4 +3,4 @@ Theorem T (C A B : Bool) : C -> A -> B -> A.
    exact.
    done.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/push.lean b/tests/lean/push.lean
index 6e0cf781b..486241470 100644
--- a/tests/lean/push.lean
+++ b/tests/lean/push.lean
@@ -10,7 +10,7 @@ Pop
 
 Eval f a -- should produce an error
 
-Show Environment 1
+print Environment 1
 
 Push
   Infixl 100 ++ : Int::add
diff --git a/tests/lean/scope.lean b/tests/lean/scope.lean
index efb8e687e..278e9800d 100644
--- a/tests/lean/scope.lean
+++ b/tests/lean/scope.lean
@@ -23,5 +23,5 @@ Scope
          in Trans L5 L3.
 EndScope
 
-Show Environment 3.
+print Environment 3.
 Eval g Int Int::sub 10 20
\ No newline at end of file
diff --git a/tests/lean/showenv.l b/tests/lean/showenv.l
index 1c1c84910..893adff90 100644
--- a/tests/lean/showenv.l
+++ b/tests/lean/showenv.l
@@ -1,3 +1,3 @@
 SetOption pp::colors  false
-Echo "===BEGIN ENVIRONMENT==="
-Show Environment
+print "===BEGIN ENVIRONMENT==="
+print Environment
diff --git a/tests/lean/single.lean b/tests/lean/single.lean
index 6a9513fa9..5ffa93ba6 100644
--- a/tests/lean/single.lean
+++ b/tests/lean/single.lean
@@ -1,6 +1,6 @@
 Import Int.
 Variables a b c : Int.
-Show a + b + c.
+print a + b + c.
 Check a + b.
 Exit.
 -- the following line should be executed
diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean
index 522e6b6f0..3259ae2d9 100644
--- a/tests/lean/subst.lean
+++ b/tests/lean/subst.lean
@@ -7,4 +7,4 @@ Theorem T : a + n + a = 10 := Subst H1 H2
 SetOption pp::coercion true
 SetOption pp::notation false
 SetOption pp::implicit true
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/subst2.lean b/tests/lean/subst2.lean
index 32d6b0efd..75c155e0f 100644
--- a/tests/lean/subst2.lean
+++ b/tests/lean/subst2.lean
@@ -12,4 +12,4 @@ Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x)
    apply (Subst (Subst H H::1) H::2)
    done.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/subst3.lean b/tests/lean/subst3.lean
index 682694278..f2eda9085 100644
--- a/tests/lean/subst3.lean
+++ b/tests/lean/subst3.lean
@@ -4,4 +4,4 @@ Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x)
    For x y z, Assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
       Subst' H1 H2 H3.
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean
index df496ea0d..d4212d2db 100644
--- a/tests/lean/tactic1.lean
+++ b/tests/lean/tactic1.lean
@@ -8,4 +8,4 @@ Variables p q r : Bool
  env:add_theorem("T1", conjecture, proof)
 *)
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean
index 2b9ac1e34..a944d5d07 100644
--- a/tests/lean/tactic10.lean
+++ b/tests/lean/tactic10.lean
@@ -21,4 +21,4 @@ Theorem T2 (a b : Bool) : (h a b) => (f b) => a := _.
      simple_tac
      done.
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/tactic13.lean b/tests/lean/tactic13.lean
index 57b048f2d..39ebb8f27 100644
--- a/tests/lean/tactic13.lean
+++ b/tests/lean/tactic13.lean
@@ -19,4 +19,4 @@ Theorem T2 (a b c : Int) (H1 : a = b) (H2 : a = c) : (f (f a c)) = (f (f b a)).
    auto.
    done.
 
-Show Environment 2.
\ No newline at end of file
+print Environment 2.
\ No newline at end of file
diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean
index 3dc86521c..1bb0e6b95 100644
--- a/tests/lean/tactic14.lean
+++ b/tests/lean/tactic14.lean
@@ -10,4 +10,4 @@ Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
    fun assumption : a = b,
       show (f (f a)) = (f (f b)) by congr_tac
 
-Show Environment 1.
+print Environment 1.
diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean
index 605cc94ef..4d255032b 100644
--- a/tests/lean/tactic2.lean
+++ b/tests/lean/tactic2.lean
@@ -21,18 +21,18 @@ Theorem T2 : p => q => p /\ q /\ p := _.
     simple_tac
     done
 
-Show Environment 1
+print Environment 1
 
 Theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
     (* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *)
     done
 
 -- Display proof term generated by previous tac
-Show Environment 1
+print Environment 1
 
 Theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
     Repeat (OrElse (apply Discharge) (apply Conj) conj_hyp exact)
     done
 
 -- Display proof term generated by previous tac --
-Show Environment 1
\ No newline at end of file
+print Environment 1
\ No newline at end of file
diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean
index 09728c16d..20048fa35 100644
--- a/tests/lean/tactic3.lean
+++ b/tests/lean/tactic3.lean
@@ -6,4 +6,4 @@ Theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
     done
 
 -- Display proof term generated by previous tactic
-Show Environment 1
\ No newline at end of file
+print Environment 1
\ No newline at end of file
diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean
index 018034fb6..509682344 100644
--- a/tests/lean/tactic4.lean
+++ b/tests/lean/tactic4.lean
@@ -6,4 +6,4 @@ Theorem T4 (a b : Bool) : a => b => a /\ b := _.
         simple_tac
         done
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean
index 5f8d8886d..c0205251e 100644
--- a/tests/lean/tactic5.lean
+++ b/tests/lean/tactic5.lean
@@ -6,4 +6,4 @@ Theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.
         simple_tac
         done
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean
index d4379d4fc..5a4007f58 100644
--- a/tests/lean/tactic8.lean
+++ b/tests/lean/tactic8.lean
@@ -6,4 +6,4 @@ Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
      exact
      absurd
      done
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean
index abb0ffedf..ef6241130 100644
--- a/tests/lean/tactic9.lean
+++ b/tests/lean/tactic9.lean
@@ -10,4 +10,4 @@ Theorem T (a b : Bool) : a \/ b => (f b) => a := _.
      absurd
      done
 
-Show Environment 1.
\ No newline at end of file
+print Environment 1.
\ No newline at end of file
diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean
index 27cecadee..ce374b70e 100644
--- a/tests/lean/tst1.lean
+++ b/tests/lean/tst1.lean
@@ -12,15 +12,15 @@ Definition const {A : Type} (n : N) (d : A) : vector A n := fun (i : N) (H : i <
 Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := fun (j : N) (H : j < n), if (j = i) d (v j H)
 Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
 Definition map {A B C : Type} {n : N} (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : N) (H : i < n), f (v1 i H) (v2 i H)
-Show Environment 10
+print Environment 10
 Check select (update (const three false) two true) two two_lt_three
 Eval select (update (const three false) two true) two two_lt_three
 Check update (const three false) two true
-Echo "\n--------"
+print "\n--------"
 Check @select
-Echo "\nmap type ---> "
+print "\nmap type ---> "
 Check @map
-Echo "\nmap normal form --> "
+print "\nmap normal form --> "
 Eval @map
-Echo "\nupdate normal form --> "
+print "\nupdate normal form --> "
 Eval @update
diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean
index a6813c71d..cb2cf313e 100644
--- a/tests/lean/tst10.lean
+++ b/tests/lean/tst10.lean
@@ -1,20 +1,20 @@
 Variable a : Bool
 Variable b : Bool
 -- Conjunctions
-Show a && b
-Show a && b && a
-Show a /\ b
-Show a ∧ b
-Show (and a b)
-Show and a b
+print a && b
+print a && b && a
+print a /\ b
+print a ∧ b
+print (and a b)
+print and a b
 -- Disjunctions
-Show a || b
-Show a \/ b
-Show a ∨ b
-Show (or a b)
-Show or a (or a b)
+print a || b
+print a \/ b
+print a ∨ b
+print (or a b)
+print or a (or a b)
 -- Simple Formulas
-Show a => b => a
+print a => b => a
 Check a => b
 Eval a => a
 Eval true => a
@@ -22,5 +22,5 @@ Eval true => a
 Axiom H1 : a
 Axiom H2 : a => b
 Check @MP
-Show MP H2 H1
+print MP H2 H1
 Check MP H2 H1
diff --git a/tests/lean/tst11.lean b/tests/lean/tst11.lean
index a1119d9c4..262d110dc 100644
--- a/tests/lean/tst11.lean
+++ b/tests/lean/tst11.lean
@@ -1,10 +1,10 @@
 Definition xor (x y : Bool) : Bool := (not x) = y
 Infixr 50 ⊕ : xor
-Show xor true false
+print xor true false
 Eval xor true true
 Eval xor true false
 Variable a : Bool
-Show a ⊕ a ⊕ a
+print a ⊕ a ⊕ a
 Check @Subst
 Theorem EM2 (a : Bool) : a \/ (not a) :=
    Case (fun x : Bool, x \/ (not x)) Trivial Trivial a
diff --git a/tests/lean/tst12.lean b/tests/lean/tst12.lean
index 74ff3a4b9..6e0a6af89 100644
--- a/tests/lean/tst12.lean
+++ b/tests/lean/tst12.lean
@@ -1,5 +1,5 @@
-Show (fun x : Bool, (fun y : Bool, x /\ y))
-Show let x := true,
+print (fun x : Bool, (fun y : Bool, x /\ y))
+print let x := true,
          y := true
      in (let z := x /\ y,
              f := (fun arg1 arg2 : Bool, arg1 /\ arg2 <=>
diff --git a/tests/lean/tst13.lean b/tests/lean/tst13.lean
index 6841ab845..2c07e525f 100644
--- a/tests/lean/tst13.lean
+++ b/tests/lean/tst13.lean
@@ -1,5 +1,5 @@
-Show fun x : Bool, (fun x : Bool, x).
-Show let x := true,
+print fun x : Bool, (fun x : Bool, x).
+print let x := true,
          y := true
      in (let z := x /\ y,
              f := (fun x y : Bool, x /\ y <=>
diff --git a/tests/lean/tst14.lean b/tests/lean/tst14.lean
index e16b45ba5..f4a2bda39 100644
--- a/tests/lean/tst14.lean
+++ b/tests/lean/tst14.lean
@@ -1,5 +1,5 @@
 Import Int.
-Show Int -> Int -> Int
+print Int -> Int -> Int
 Variable f : Int -> Int -> Int
 Eval f 0
 Check f 0
diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean
index 5c1256f24..6940b3ebe 100644
--- a/tests/lean/tst15.lean
+++ b/tests/lean/tst15.lean
@@ -6,15 +6,15 @@ Check f x
 Check (Type 4)
 Check x
 Check (Type max U M)
-Show (Type U+3)
+print (Type U+3)
 Check (Type U+3)
 Check (Type U ⊔ M)
 Check (Type U ⊔ M ⊔ 3)
-Show (Type U+1 ⊔ M ⊔ 3)
+print (Type U+1 ⊔ M ⊔ 3)
 Check (Type U+1 ⊔ M ⊔ 3)
-Show (Type U) -> (Type 5)
+print (Type U) -> (Type 5)
 Check (Type U) -> (Type 5)
 Check (Type M ⊔ 3) -> (Type U+5)
-Show (Type M ⊔ 3) -> (Type U) -> (Type 5)
+print (Type M ⊔ 3) -> (Type U) -> (Type 5)
 Check (Type M ⊔ 3) -> (Type U) -> (Type 5)
-Show (Type U)
+print (Type U)
diff --git a/tests/lean/tst16.lean b/tests/lean/tst16.lean
index ce0732e90..76c48160e 100644
--- a/tests/lean/tst16.lean
+++ b/tests/lean/tst16.lean
@@ -1,15 +1,15 @@
 Variable f : Type -> Bool
-Show forall a b : Type, (f a) = (f b)
+print forall a b : Type, (f a) = (f b)
 Variable g : Bool -> Bool -> Bool
-Show forall (a b : Type) (c : Bool), g c ((f a) = (f b))
-Show exists (a b : Type) (c : Bool), g c ((f a) = (f b))
-Show forall (a b : Type) (c : Bool), (g c (f a) = (f b)) ⇒ (f a)
+print forall (a b : Type) (c : Bool), g c ((f a) = (f b))
+print exists (a b : Type) (c : Bool), g c ((f a) = (f b))
+print forall (a b : Type) (c : Bool), (g c (f a) = (f b)) ⇒ (f a)
 Check forall (a b : Type) (c : Bool), g c ((f a) = (f b))
-Show ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
-Show ∀ a b : Type, (f a) = (f b)
-Show ∃ a b : Type, (f a) = (f b) ∧ (f a)
-Show ∃ a b : Type, (f a) = (f b) ∨ (f b)
+print ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+print ∀ a b : Type, (f a) = (f b)
+print ∃ a b : Type, (f a) = (f b) ∧ (f a)
+print ∃ a b : Type, (f a) = (f b) ∨ (f b)
 Variable a : Bool
-Show (f a) ∨ (f a)
-Show (f a) = a ∨ (f a)
-Show (f a) = a ∧ (f a)
+print (f a) ∨ (f a)
+print (f a) = a ∨ (f a)
+print (f a) = a ∧ (f a)
diff --git a/tests/lean/tst17.lean b/tests/lean/tst17.lean
index c335b8f2e..509c86d3a 100644
--- a/tests/lean/tst17.lean
+++ b/tests/lean/tst17.lean
@@ -1,5 +1,5 @@
 Variable f : Type -> Bool
 Variable g : Type -> Type -> Bool
-Show forall (a b : Type), exists (c : Type), (g a b) = (f c)
+print forall (a b : Type), exists (c : Type), (g a b) = (f c)
 Check forall (a b : Type), exists (c : Type), (g a b) = (f c)
 Eval forall (a b : Type), exists (c : Type), (g a b) = (f c)
diff --git a/tests/lean/tst2.lean b/tests/lean/tst2.lean
index 716770211..7aa3ba63b 100644
--- a/tests/lean/tst2.lean
+++ b/tests/lean/tst2.lean
@@ -1,11 +1,11 @@
-Show Options
+print Options
 Variable a : Bool
 Variable b : Bool
-Show a/\b
+print a/\b
 SetOption lean::pp::notation false
-Show Options
-Show a/\b
-Show Environment 2
+print Options
+print a/\b
+print Environment 2
 SetOption lean::pp::notation true
-Show Options
-Show a/\b
+print Options
+print a/\b
diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean
index b0e69e680..310f2d0b5 100644
--- a/tests/lean/tst3.lean
+++ b/tests/lean/tst3.lean
@@ -1,58 +1,58 @@
 SetOption lean::parser::verbose false.
 Notation 10 if _ then _ : implies.
-Show Environment 1.
-Show if true then false.
+print Environment 1.
+print if true then false.
 Variable a : Bool.
-Show if true then if a then false.
+print if true then if a then false.
 SetOption lean::pp::notation false.
-Show if true then if a then false.
+print if true then if a then false.
 Variable A : Type.
 Variable f : A -> A -> A -> Bool.
 Notation 100  _ |- _ ; _  : f.
-Show Environment 1.
+print Environment 1.
 Variable c : A.
 Variable d : A.
 Variable e : A.
-Show c |- d ; e.
+print c |- d ; e.
 SetOption lean::pp::notation true.
-Show c |- d ; e.
+print c |- d ; e.
 Variable fact : A -> A.
 Notation 20 _ ! : fact.
-Show c! !.
+print c! !.
 SetOption lean::pp::notation false.
-Show c! !.
+print c! !.
 SetOption lean::pp::notation true.
 Variable g : A -> A -> A.
 Notation 30 [ _ ; _ ] : g
-Show [c;d].
-Show [c ; [d;e] ].
+print [c;d].
+print [c ; [d;e] ].
 SetOption lean::pp::notation false.
-Show [c ; [d;e] ].
+print [c ; [d;e] ].
 SetOption lean::pp::notation true.
 Variable h : A -> A -> A.
 Notation 40 _ << _ end : h.
-Show Environment 1.
-Show d << e end.
-Show [c ; d << e end ].
+print Environment 1.
+print d << e end.
+print [c ; d << e end ].
 SetOption lean::pp::notation false.
-Show [c ; d << e end ].
+print [c ; d << e end ].
 SetOption lean::pp::notation true.
 Variable r : A -> A -> A.
 Infixl 30 ++ : r.
 Variable s : A -> A -> A.
 Infixl 40 ** : s.
-Show c ** d ++ e ** c.
+print c ** d ++ e ** c.
 Variable p1 : Bool.
 Variable p2 : Bool.
 Variable p3 : Bool.
-Show p1 || p2 && p3.
+print p1 || p2 && p3.
 SetOption lean::pp::notation false.
-Show c ** d ++ e ** c.
-Show p1 || p2 && p3.
+print c ** d ++ e ** c.
+print p1 || p2 && p3.
 SetOption lean::pp::notation true.
-Show c = d || d = c.
-Show  not p1 || p2.
-Show p1 && p3 || p2 && p3.
+print c = d || d = c.
+print  not p1 || p2.
+print p1 && p3 || p2 && p3.
 SetOption lean::pp::notation false.
-Show  not p1 || p2.
-Show p1 && p3 || p2 && p3.
+print  not p1 || p2.
+print p1 && p3 || p2 && p3.
diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean
index 4bbbc8f70..72f3a17d2 100644
--- a/tests/lean/tst4.lean
+++ b/tests/lean/tst4.lean
@@ -3,14 +3,14 @@ Variable N : Type
 Variable n1 : N
 Variable n2 : N
 SetOption lean::pp::implicit true
-Show f n1 n2
-Show f (fun x : N -> N, x) (fun y : _, y)
+print f n1 n2
+print f (fun x : N -> N, x) (fun y : _, y)
 Variable EqNice {A : Type} (lhs rhs : A) : Bool
 Infix 50 === : EqNice
-Show n1 === n2
+print n1 === n2
 Check f n1 n2
 Check @Congr
-Show f n1 n2
+print f n1 n2
 Variable a : N
 Variable b : N
 Variable c : N
@@ -18,4 +18,4 @@ Variable g : N -> N
 Axiom H1 : a = b && b = c
 Theorem Pr : (g a) = (g c) :=
     Congr (Refl g) (Trans (Conjunct1 H1) (Conjunct2 H1))
-Show Environment 2
+print Environment 2
diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean
index 75befcf6d..00d8dcc49 100644
--- a/tests/lean/tst5.lean
+++ b/tests/lean/tst5.lean
@@ -1,9 +1,9 @@
 Variable N : Type
 Variable a : N
 Variable b : N
-Show a = b
+print a = b
 Check a = b
 SetOption lean::pp::implicit true
-Show a = b
-Show (Type 1) = (Type 1)
-Show true = false
+print a = b
+print (Type 1) = (Type 1)
+print true = false
diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean
index 74c05a378..ad0a0a085 100644
--- a/tests/lean/tst6.lean
+++ b/tests/lean/tst6.lean
@@ -6,11 +6,11 @@ Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h
 
 -- Display the theorem showing implicit arguments
 SetOption lean::pp::implicit true
-Show Environment 2
+print Environment 2
 
 -- Display the theorem hiding implicit arguments
 SetOption lean::pp::implicit false
-Show Environment 2
+print Environment 2
 
 Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
     DisjCases H
@@ -19,9 +19,9 @@ Theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
               (fun H1 : a = d ∧ d = c,
                    CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
 
--- Show proof of the last theorem with all implicit arguments
+-- print proof of the last theorem with all implicit arguments
 SetOption lean::pp::implicit true
-Show Environment 1
+print Environment 1
 
 -- Using placeholders to hide the type of H1
 Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
@@ -32,7 +32,7 @@ Theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h
                    CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
 
 SetOption lean::pp::implicit true
-Show Environment 1
+print Environment 1
 
 -- Same example but the first conjuct has unnecessary stuff
 Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) :=
@@ -43,7 +43,7 @@ Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
                    CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
 
 SetOption lean::pp::implicit false
-Show Environment 1
+print Environment 1
 
 Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
     DisjCases H
@@ -55,4 +55,4 @@ Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
                    in CongrH AeqC (Symm AeqC))
 
 SetOption lean::pp::implicit false
-Show Environment 1
+print Environment 1
diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean
index 724c8557b..427ffa77c 100644
--- a/tests/lean/tst7.lean
+++ b/tests/lean/tst7.lean
@@ -1,10 +1,10 @@
 Variable f : Pi (A : Type), A -> Bool
-Show fun (A B : Type) (a : _), f B a
+print fun (A B : Type) (a : _), f B a
 -- The following one should produce an error
-Show fun (A : Type) (a : _) (B : Type), f B a
+print fun (A : Type) (a : _) (B : Type), f B a
 
 Variable myeq : Pi A : (Type U), A -> A -> Bool
-Show  myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
+print  myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
 Check myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
 
 
diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out
index 26065b95d..cfd1737bf 100644
--- a/tests/lean/tst7.lean.expected.out
+++ b/tests/lean/tst7.lean.expected.out
@@ -4,7 +4,7 @@
 λ (A B : Type) (a : B), f B a
 Failed to solve
 A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B
-    (line: 4: pos: 41) Type of argument 2 must be convertible to the expected type in the application of
+    (line: 4: pos: 42) Type of argument 2 must be convertible to the expected type in the application of
         f
     with arguments:
         B
diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean
index a873c2fa8..8b17d278e 100644
--- a/tests/lean/tst8.lean
+++ b/tests/lean/tst8.lean
@@ -10,5 +10,5 @@ Definition f (A: Type) (a : A) : A :=
        c := g A b
    in c
 
-Show f _ 10.
-Show f _ (- 10).
+print f _ 10.
+print f _ (- 10).
diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean
index 7e86bf989..33a56f089 100644
--- a/tests/lean/unicode.lean
+++ b/tests/lean/unicode.lean
@@ -1,8 +1,8 @@
-Show true /\ false
+print true /\ false
 SetOption pp::unicode false
-Show true /\ false
+print true /\ false
 SetOption pp::unicode true
 SetOption lean::pp::notation false
-Show true /\ false
+print true /\ false
 SetOption pp::unicode false
-Show true /\ false
+print true /\ false
diff --git a/tests/lua/coercion_bug1.lua b/tests/lua/coercion_bug1.lua
index 5c19e8125..5b442ad49 100644
--- a/tests/lua/coercion_bug1.lua
+++ b/tests/lua/coercion_bug1.lua
@@ -3,9 +3,9 @@ env:import("Int")
 parse_lean_cmds([[
   Variable f : Int -> Int -> Int
   Notation 20 _ +++ _ : f
-  Show f 10 20
+  print f 10 20
   Notation 20 _ -+- _ : f
-  Show f 10 20
+  print f 10 20
 ]], env)
 
 local F = parse_lean('f 10 20', env)
@@ -15,7 +15,7 @@ assert(tostring(lean_formatter(env)(F)) == "10 -+- 20")
 local child = env:mk_child()
 
 parse_lean_cmds([[
-  Show f 10 20
+  print f 10 20
 ]], child)
 
 assert(tostring(lean_formatter(env)(F)) == "10 -+- 20")
diff --git a/tests/lua/front.lua b/tests/lua/front.lua
index fc7627730..42a214424 100644
--- a/tests/lua/front.lua
+++ b/tests/lua/front.lua
@@ -17,8 +17,8 @@ print(get_options())
 assert(get_options():get{"pp", "colors"})
 assert(get_options():get{"pp", "width"} == 300)
 parse_lean_cmds([[
-  Show i ++ j
-  Show f i j
+  print i ++ j
+  print f i j
 ]], env)
 
 local env2 = environment()
@@ -26,7 +26,7 @@ env2:import("Int")
 parse_lean_cmds([[
 Variable f : Int -> Int -> Int
 Variables a b : Int
-Show f a b
+print f a b
 Notation 100 _ -+ _ : f
 ]], env2)
 
@@ -41,7 +41,7 @@ local fmt = lean_formatter(env)
 -- We can parse commands with respect to environment env2,
 -- but using a formatter based on env.
 parse_lean_cmds([[
-Show f a b
+print f a b
 ]], env2, options(), fmt)
 
 set_formatter(fmt)