From 4946f5529085a38332110905fa61739e86b504f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Oct 2014 16:20:52 -0700
Subject: [PATCH] refactor(frontends/lean): constant/axiom are top-level
 commands, parameter/variable/hypothesis/conjecture are section/context-level
 commands

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/lean/calc.org                     |   3 +-
 doc/lean/tutorial.org                 |  66 +++++++-------
 library/data/list/basic.lean          |   2 +-
 library/data/vector.lean              |   2 +-
 src/emacs/lean-syntax.el              |   4 +-
 src/frontends/lean/decl_cmds.cpp      | 122 +++++++++++++++++---------
 src/frontends/lean/token_table.cpp    |   5 +-
 tests/lean/alias.lean                 |  10 +--
 tests/lean/bug1.lean                  |   2 +-
 tests/lean/calc1.lean                 |  14 +--
 tests/lean/choice_expl.lean           |   4 +-
 tests/lean/coe.lean                   |   2 +-
 tests/lean/have1.lean                 |   2 +-
 tests/lean/inst.lean                  |   2 +-
 tests/lean/interactive/coe.lean       |   4 +-
 tests/lean/let3.lean                  |   2 +-
 tests/lean/let4.lean                  |   2 +-
 tests/lean/num2.lean                  |  16 ++--
 tests/lean/num3.lean                  |   8 +-
 tests/lean/num4.lean                  |   8 +-
 tests/lean/run/abs.lean               |   4 +-
 tests/lean/run/algebra1.lean          |   8 +-
 tests/lean/run/alias1.lean            |  14 +--
 tests/lean/run/alias2.lean            |  12 +--
 tests/lean/run/alias3.lean            |   2 +-
 tests/lean/run/basic.lean             |  14 +--
 tests/lean/run/bug6.lean              |   8 +-
 tests/lean/run/calc.lean              |   2 +-
 tests/lean/run/class11.lean           |   4 +-
 tests/lean/run/class4.lean            |   4 +-
 tests/lean/run/class5.lean            |  12 +--
 tests/lean/run/class_coe.lean         |  22 ++---
 tests/lean/run/coe1.lean              |  14 +--
 tests/lean/run/coe10.lean             |   6 +-
 tests/lean/run/coe11.lean             |  12 +--
 tests/lean/run/coe12.lean             |   4 +-
 tests/lean/run/coe13.lean             |   6 +-
 tests/lean/run/coe14.lean             |   6 +-
 tests/lean/run/coe6.lean              |  12 +--
 tests/lean/run/coe7.lean              |   6 +-
 tests/lean/run/coe8.lean              |  12 +--
 tests/lean/run/coe9.lean              |  24 ++---
 tests/lean/run/coefun.lean            |   6 +-
 tests/lean/run/ctx.lean               |   6 +-
 tests/lean/run/decidable.lean         |   4 +-
 tests/lean/run/e1.lean                |  12 +--
 tests/lean/run/e10.lean               |  16 ++--
 tests/lean/run/e11.lean               |  14 +--
 tests/lean/run/e12.lean               |  14 +--
 tests/lean/run/e13.lean               |  12 +--
 tests/lean/run/e14.lean               |   4 +-
 tests/lean/run/e15.lean               |   2 +-
 tests/lean/run/e16.lean               |   2 +-
 tests/lean/run/e17.lean               |   4 +-
 tests/lean/run/e18.lean               |   6 +-
 tests/lean/run/e5.lean                |   2 +-
 tests/lean/run/e6.lean                |  14 +--
 tests/lean/run/e7.lean                |  14 +--
 tests/lean/run/e8.lean                |  14 +--
 tests/lean/run/e9.lean                |  14 +--
 tests/lean/run/elim.lean              |   2 +-
 tests/lean/run/elim2.lean             |   2 +-
 tests/lean/run/export.lean            |   2 +-
 tests/lean/run/full.lean              |   2 +-
 tests/lean/run/fun.lean               |  10 +--
 tests/lean/run/group.lean             |   8 +-
 tests/lean/run/group2.lean            |  22 ++---
 tests/lean/run/have1.lean             |   2 +-
 tests/lean/run/have2.lean             |   2 +-
 tests/lean/run/have3.lean             |   2 +-
 tests/lean/run/have4.lean             |   2 +-
 tests/lean/run/have5.lean             |   2 +-
 tests/lean/run/have6.lean             |   6 +-
 tests/lean/run/imp.lean               |   8 +-
 tests/lean/run/impbug1.lean           |   2 +-
 tests/lean/run/impbug2.lean           |   8 +-
 tests/lean/run/impbug3.lean           |   8 +-
 tests/lean/run/impbug4.lean           |   8 +-
 tests/lean/run/implicit.lean          |   4 +-
 tests/lean/run/ind_bug.lean           |   4 +-
 tests/lean/run/induniv.lean           |   2 +-
 tests/lean/run/local_using.lean       |  12 +--
 tests/lean/run/match1.lean            |   2 +-
 tests/lean/run/match2.lean            |   4 +-
 tests/lean/run/matrix.lean            |   6 +-
 tests/lean/run/matrix2.lean           |   6 +-
 tests/lean/run/n1.lean                |  10 +--
 tests/lean/run/n2.lean                |   8 +-
 tests/lean/run/n3.lean                |  14 +--
 tests/lean/run/n4.lean                |  10 +--
 tests/lean/run/n5.lean                |  12 +--
 tests/lean/run/nat_bug2.lean          |   2 +-
 tests/lean/run/nat_bug3.lean          |   2 +-
 tests/lean/run/nat_bug6.lean          |   2 +-
 tests/lean/run/nat_coe.lean           |  14 +--
 tests/lean/run/not_bug1.lean          |   8 +-
 tests/lean/run/ns.lean                |  16 ++--
 tests/lean/run/ns2.lean               |   2 +-
 tests/lean/run/occurs_check_bug1.lean |   4 +-
 tests/lean/run/opaque_hint_bug.lean   |   2 +-
 tests/lean/run/over_subst.lean        |  16 ++--
 tests/lean/run/root.lean              |   6 +-
 tests/lean/run/secnot.lean            |   2 +-
 tests/lean/run/section2.lean          |   4 +-
 tests/lean/run/t11.lean               |   8 +-
 tests/lean/run/t3.lean                |  16 ++--
 tests/lean/run/t4.lean                |   2 +-
 tests/lean/run/t5.lean                |  10 +--
 tests/lean/run/t6.lean                |   6 +-
 tests/lean/run/t7.lean                |   6 +-
 tests/lean/run/tactic15.lean          |   4 +-
 tests/lean/run/tactic16.lean          |   4 +-
 tests/lean/run/tactic17.lean          |   4 +-
 tests/lean/run/tactic18.lean          |   4 +-
 tests/lean/run/uni2.lean              |   2 +-
 tests/lean/run/unicode.lean           |  10 +--
 tests/lean/run/univ1.lean             |  16 ++--
 tests/lean/run/univ2.lean             |   8 +-
 tests/lean/show1.lean                 |   2 +-
 tests/lean/slow/list_elab2.lean       |   2 +-
 tests/lean/t10.lean                   |  24 ++---
 tests/lean/t11.lean                   |   8 +-
 tests/lean/t12.lean                   |   6 +-
 tests/lean/t13.lean                   |  12 +--
 tests/lean/t14.lean                   |  10 +--
 tests/lean/t4.lean                    |  26 +++---
 tests/lean/t5.lean                    |   6 +-
 tests/lean/t7.lean                    |   2 +-
 tests/lean/t9.lean                    |  10 +--
 tests/lean/uni_bug1.lean              |   4 +-
 130 files changed, 583 insertions(+), 549 deletions(-)

diff --git a/doc/lean/calc.org b/doc/lean/calc.org
index 7d6d179d1..c74bf35f8 100644
--- a/doc/lean/calc.org
+++ b/doc/lean/calc.org
@@ -1,6 +1,5 @@
 * Calculational Proofs
 
-
 A calculational proof is just a chain of intermediate results that are
 meant to be composed by basic principles such as the transitivity of
 ===. In Lean, a calculation proof starts with the keyword =calc=, and has
@@ -27,7 +26,7 @@ Here is an example
 #+BEGIN_SRC lean
   import data.nat
   open nat
-  variables a b c d e : nat.
+  constants a b c d e : nat.
   axiom Ax1 : a = b.
   axiom Ax2 : b = c + 1.
   axiom Ax3 : c = d.
diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index 03bcd8da2..4b8363ef8 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -74,21 +74,21 @@ the following command creates aliases for all objects starting with
   check ge -- display the type of nat.ge
 #+END_SRC
 
-The command =variable= assigns a type to an identifier. The following command postulates/assumes
+The command =constant= assigns a type to an identifier. The following command postulates/assumes
 that =n=, =m= and =o= have type =nat=.
 
 #+BEGIN_SRC lean
   import data.nat
   open nat
-  variable n : nat
-  variable m : nat
-  variable o : nat
+  constant n : nat
+  constant m : nat
+  constant o : nat
   -- The command 'open nat' also imported the notation defined at the namespace 'nat'
   check n + m
   check n ≤ m
 #+END_SRC
 
-The command =variables n m o : nat= can be used as a shorthand for the three commands above.
+The command =constants n m o : nat= can be used as a shorthand for the three commands above.
 
 In Lean, proofs are also expressions, and all functionality provided for manipulating
 expressions is also available for manipulating proofs. For example, =eq.refl n= is a proof
@@ -97,7 +97,7 @@ for =n = n=. In Lean, =eq.refl= is the reflexivity theorem.
 #+BEGIN_SRC lean
   import data.nat
   open nat
-  variable n : nat
+  constant n : nat
   check eq.refl n
 #+END_SRC
 
@@ -109,7 +109,7 @@ The following commands postulate two axioms =Ax1= and =Ax2= that state that =n =
 #+BEGIN_SRC lean
   import data.nat
   open nat
-  variables m n o : nat
+  constants m n o : nat
   axiom Ax1 : n = m
   axiom Ax2 : m = o
   check eq.trans Ax1 Ax2
@@ -132,13 +132,13 @@ and =em p= is a proof for =p ∨ ¬ p=.
 
 #+BEGIN_SRC lean
   import logic.axioms.classical
-  variable p : Prop
+  constant p : Prop
   check em p
 #+END_SRC
 
-The commands =axiom= and =variable= are essentially the same command. We provide both
+The commands =axiom= and =constant= are essentially the same command. We provide both
 just to make Lean files more readable. We encourage users to use =axiom= only for
-propositions, and =variable= for everything else.
+propositions, and =constant= for everything else.
 
 Similarly, a theorem is just a definition. The following command defines a new theorem
 called =nat_trans3=, and then use it to prove something else. In this
@@ -152,7 +152,7 @@ example, =eq.symm= is the symmetry theorem.
   eq.trans (eq.trans H1 (eq.symm H2)) H3
 
   -- Example using nat_trans3
-  variables x y z w : nat
+  constants x y z w : nat
   axiom Hxy : x = y
   axiom Hzy : z = y
   axiom Hzw : z = w
@@ -181,7 +181,7 @@ implicit arguments.
   eq.trans (eq.trans H1 (eq.symm H2)) H3
 
   -- Example using nat_trans3
-  variables x y z w : nat
+  constants x y z w : nat
   axiom Hxy : x = y
   axiom Hzy : z = y
   axiom Hzw : z = w
@@ -212,7 +212,7 @@ This is useful when debugging non-trivial problems.
   import data.nat
   open nat
 
-  variables a b c : nat
+  constants a b c : nat
   axiom H1 : a = b
   axiom H2 : b = c
   check eq.trans H1 H2
@@ -302,7 +302,7 @@ Here is a simple example using the connectives above.
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   check p → q → p ∧ q
   check ¬p → p ↔ false
   check p ∨ q → q ∨ p
@@ -318,7 +318,7 @@ change this behavior.
 #+BEGIN_SRC lean
   import logic
   set_option pp.unicode false
-  variables p q : Prop
+  constants p q : Prop
   check p → q → p ∧ q
   set_option pp.unicode true
   check p → q → p ∧ q
@@ -330,7 +330,7 @@ of the functions that given a proof for =p=, returns a proof for =q=. This is ve
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   -- Hpq is a function that takes a proof for p and returns a proof for q
   axiom Hpq : p → q
   -- Hq is a proof/certificate for p
@@ -405,7 +405,7 @@ For example, a proof for =p → p= is just =fun H : p, H= (the identity function
 
 #+BEGIN_SRC lean
   import logic
-  variable p : Prop
+  constant p : Prop
   check fun H : p, H
 #+END_SRC
 
@@ -450,7 +450,7 @@ In the following example we use =and.intro= for creating a proof for
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   check fun (Hp : p) (Hq : q), and.intro Hp Hq
 #+END_SRC
 
@@ -459,7 +459,7 @@ Similarly =and.elim_right H= is a proof for =b=. We say they are the _left/right
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   -- Proof for p ∧ q → p
   check fun H : p ∧ q, and.elim_left H
   -- Proof for p ∧ q → q
@@ -470,7 +470,7 @@ Now, we prove =p ∧ q → q ∧ p= with the following simple proof term.
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   check fun H : p ∧ q, and.intro (and.elim_right H) (and.elim_left H)
 #+END_SRC
 
@@ -485,7 +485,7 @@ We say they are the _left/right or-introduction_.
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   -- Proof for p → p ∨ q
   check fun H : p, or.intro_left q H
   -- Proof for q → p ∨ q
@@ -500,7 +500,7 @@ In the following example, we use =or.elim= to prove that =p v q → q ∨ p=.
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   check fun H : p ∨ q,
            or.elim H
               (fun Hp : p, or.intro_right q Hp)
@@ -516,7 +516,7 @@ the Lean standard library.
 
 #+BEGIN_SRC lean
   import logic
-  variables p q : Prop
+  constants p q : Prop
   check fun H : p ∨ q,
            or.elim H
               (fun Hp : p, or.inr Hp)
@@ -535,7 +535,7 @@ We now use =not_intro= and =absurd= to produce a proof term for
 
 #+BEGIN_SRC lean
   import logic
-  variables a b : Prop
+  constants a b : Prop
   check fun (Hab : a → b) (Hnb : ¬ b),
             not_intro (fun Ha : a, absurd (Hab Ha) Hnb)
 
@@ -547,7 +547,7 @@ explicitly.
 
 #+BEGIN_SRC lean
   import logic
-  variables a b : Prop
+  constants a b : Prop
   check fun (Hab : a → b) (Hnb : ¬ b),
             (fun Ha : a, Hnb (Hab Ha))
 
@@ -557,7 +557,7 @@ Now, here is the proof term for =¬a → b → (b → a) → c=
 
 #+BEGIN_SRC lean
   import logic
-  variables a b c : Prop
+  constants a b c : Prop
   check fun (Hna : ¬ a) (Hb : b) (Hba : b → a),
             absurd (Hba Hb) Hna
 #+END_SRC
@@ -571,7 +571,7 @@ Here is the proof term for =a ∧ b ↔ b ∧ a=
 
 #+BEGIN_SRC lean
   import logic
-  variables a b : Prop
+  constants a b : Prop
   check iff.intro
           (fun H : a ∧ b, and.intro (and.elim_right H) (and.elim_left H))
           (fun H : b ∧ a, and.intro (and.elim_right H) (and.elim_left H))
@@ -582,7 +582,7 @@ more like proofs found in text books.
 
 #+BEGIN_SRC lean
   import logic
-  variables a b : Prop
+  constants a b : Prop
   check iff.intro
           (assume H : a ∧ b, and.intro (and.elim_right H) (and.elim_left H))
           (assume H : b ∧ a, and.intro (and.elim_right H) (and.elim_left H))
@@ -654,10 +654,10 @@ Then we instantiate the axiom using function application.
   import data.nat
   open nat
 
-  variable f : nat → nat
+  constant f : nat → nat
   axiom fzero : ∀ x, f x = 0
   check fzero 1
-  variable a : nat
+  constant a : nat
   check fzero a
 #+END_SRC
 
@@ -670,7 +670,7 @@ abstraction. In the following example, we create a proof term showing that for a
   import data.nat
   open nat
 
-  variable f : nat → nat
+  constant f : nat → nat
   axiom fzero : ∀ x, f x = 0
   check λ x y, eq.trans (fzero x) (eq.symm (fzero y))
 #+END_SRC
@@ -698,7 +698,7 @@ for =∃ a : nat, a = w= using
   theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
   eq.trans (eq.trans H1 (eq.symm H2)) H3
 
-  variables x y z w : nat
+  constants x y z w : nat
   axiom Hxy : x = y
   axiom Hzy : z = y
   axiom Hzw : z = w
@@ -723,7 +723,7 @@ has different values for the implicit argument =P=.
   open nat
 
   check @exists_intro
-  variable g : nat → nat → nat
+  constant g : nat → nat → nat
   axiom Hg : g 0 0 = 0
   theorem gex1 : ∃ x, g x x = x := exists_intro 0 Hg
   theorem gex2 : ∃ x, g x 0 = x := exists_intro 0 Hg
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index bbcd056b1..a4ba561ac 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -27,7 +27,7 @@ infix `::` := cons
 
 section
 
-variable {T : Type}
+parameter {T : Type}
 
 protected theorem induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hind : ∀ (x : T) (l : list T),  P l → P (x::l)) : P l :=
diff --git a/library/data/vector.lean b/library/data/vector.lean
index c6e14b056..8a3821636 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -13,7 +13,7 @@ namespace vector
   notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
   section sc_vector
-  variable {T : Type}
+  parameter {T : Type}
 
   protected theorem rec_on {C : ∀ (n : ℕ), vector T n → Type} {n : ℕ} (v : vector T n) (Hnil : C 0 nil)
     (Hcons : ∀(x : T) {n : ℕ} (w : vector T n), C n w → C (succ n) (cons x w)) : C n v :=
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 3a0ababde..03b24f9fd 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -9,7 +9,7 @@
 
 (defconst lean-keywords
   '("import" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
-    "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
+    "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
@@ -105,7 +105,7 @@
      ;; universe/inductive/theorem... "names"
      (,(rx word-start
            (group (or "universe" "inductive" "theorem" "axiom" "lemma" "hypothesis"
-                      "definition" "variable" "parameter"))
+                      "definition" "variable" "constant" "parameter"))
            word-end
            (zero-or-more (or whitespace "(" "{" "["))
            (group (zero-or-more (not whitespace))))
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 7936d3bf7..2a5ce2b57 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -64,9 +64,11 @@ void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found, pa
         });
 }
 
+enum class variable_kind { Constant, Parameter, Variable, Axiom };
+
 static environment declare_var(parser & p, environment env,
                                name const & n, level_param_names const & ls, expr const & type,
-                               bool is_axiom, optional<binder_info> const & _bi, pos_info const & pos) {
+                               variable_kind k, optional<binder_info> const & _bi, pos_info const & pos) {
     binder_info bi;
     if (_bi) bi = *_bi;
     if (in_section_or_context(p.env())) {
@@ -77,7 +79,7 @@ static environment declare_var(parser & p, environment env,
     } else {
         name const & ns = get_namespace(env);
         name full_n  = ns + n;
-        if (is_axiom) {
+        if (k == variable_kind::Axiom) {
             env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
             p.add_decl_index(full_n, pos, get_axiom_tk(), type);
         } else {
@@ -105,7 +107,20 @@ optional<binder_info> parse_binder_info(parser & p) {
     return bi;
 }
 
-environment variable_cmd_core(parser & p, bool is_axiom) {
+static void check_variable_kind(parser & p, variable_kind k) {
+    if (in_section_or_context(p.env())) {
+        if (k == variable_kind::Axiom || k == variable_kind::Constant)
+            throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts",
+                               p.pos());
+    } else {
+        if (k == variable_kind::Parameter || k == variable_kind::Variable)
+            throw parser_error("invalid declaration, 'parameter/variable/hypothesis/conjecture' "
+                               "can only be used in sections/contexts", p.pos());
+    }
+}
+
+environment variable_cmd_core(parser & p, variable_kind k) {
+    check_variable_kind(p, k);
     auto pos = p.pos();
     optional<binder_info> bi = parse_binder_info(p);
     name n = p.check_id_next("invalid declaration, identifier expected");
@@ -139,14 +154,66 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
     list<expr> ctx = locals_to_context(type, p);
     std::tie(type, new_ls) = p.elaborate_type(type, ctx);
     update_section_local_levels(p, new_ls);
-    return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos);
+    return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);
 }
 environment variable_cmd(parser & p) {
-    return variable_cmd_core(p, false);
+    return variable_cmd_core(p, variable_kind::Variable);
 }
 environment axiom_cmd(parser & p)    {
-    return variable_cmd_core(p, true);
+    return variable_cmd_core(p, variable_kind::Axiom);
 }
+environment constant_cmd(parser & p)    {
+    return variable_cmd_core(p, variable_kind::Constant);
+}
+environment parameter_cmd(parser & p)    {
+    return variable_cmd_core(p, variable_kind::Parameter);
+}
+
+static environment variables_cmd_core(parser & p, variable_kind k) {
+    check_variable_kind(p, k);
+    auto pos = p.pos();
+    environment env = p.env();
+    while (true) {
+        optional<binder_info> bi = parse_binder_info(p);
+        buffer<name> ids;
+        while (!p.curr_is_token(get_colon_tk())) {
+            name id = p.check_id_next("invalid parameters declaration, identifier expected");
+            ids.push_back(id);
+        }
+        p.next();
+        optional<parser::local_scope> scope1;
+        if (!in_section_or_context(p.env()))
+            scope1.emplace(p);
+        expr type = p.parse_expr();
+        p.parse_close_binder_info(bi);
+        level_param_names ls = to_level_param_names(collect_univ_params(type));
+        list<expr> ctx = locals_to_context(type, p);
+        for (auto id : ids) {
+            // Hack: to make sure we get different universe parameters for each parameter.
+            // Alternative: elaborate once and copy types replacing universes in new_ls.
+            level_param_names new_ls;
+            expr new_type;
+            std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
+            update_section_local_levels(p, new_ls);
+            new_ls = append(ls, new_ls);
+            env = declare_var(p, env, id, new_ls, new_type, k, bi, pos);
+        }
+        if (!p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lcurly_tk()) &&
+            !p.curr_is_token(get_ldcurly_tk()) && !p.curr_is_token(get_lbracket_tk()))
+            break;
+    }
+    return env;
+}
+static environment variables_cmd(parser & p) {
+    return variables_cmd_core(p, variable_kind::Variable);
+}
+static environment parameters_cmd(parser & p) {
+    return variables_cmd_core(p, variable_kind::Parameter);
+}
+static environment constants_cmd(parser & p) {
+    return variables_cmd_core(p, variable_kind::Constant);
+}
+
 
 struct decl_modifiers {
     bool               m_is_instance;
@@ -403,50 +470,19 @@ environment protected_definition_cmd(parser & p) {
     return definition_cmd_core(p, is_theorem, is_opaque, false, true);
 }
 
-static environment variables_cmd(parser & p) {
-    auto pos = p.pos();
-    environment env = p.env();
-    while (true) {
-        optional<binder_info> bi = parse_binder_info(p);
-        buffer<name> ids;
-        while (!p.curr_is_token(get_colon_tk())) {
-            name id = p.check_id_next("invalid parameters declaration, identifier expected");
-            ids.push_back(id);
-        }
-        p.next();
-        optional<parser::local_scope> scope1;
-        if (!in_section_or_context(p.env()))
-            scope1.emplace(p);
-        expr type = p.parse_expr();
-        p.parse_close_binder_info(bi);
-        level_param_names ls = to_level_param_names(collect_univ_params(type));
-        list<expr> ctx = locals_to_context(type, p);
-        for (auto id : ids) {
-            // Hack: to make sure we get different universe parameters for each parameter.
-            // Alternative: elaborate once and copy types replacing universes in new_ls.
-            level_param_names new_ls;
-            expr new_type;
-            std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
-            update_section_local_levels(p, new_ls);
-            new_ls = append(ls, new_ls);
-            env = declare_var(p, env, id, new_ls, new_type, false, bi, pos);
-        }
-        if (!p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lcurly_tk()) &&
-            !p.curr_is_token(get_ldcurly_tk()) && !p.curr_is_token(get_lbracket_tk()))
-            break;
-    }
-    return env;
-}
-
 void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("universe",     "declare a global universe level", universe_cmd));
-    add_cmd(r, cmd_info("variable",     "declare a new parameter", variable_cmd));
+    add_cmd(r, cmd_info("variable",     "declare a new variable", variable_cmd));
+    add_cmd(r, cmd_info("parameter",    "declare a new parameter", parameter_cmd));
+    add_cmd(r, cmd_info("constant",     "declare a new constant (aka top-level variable)", constant_cmd));
     add_cmd(r, cmd_info("axiom",        "declare a new axiom", axiom_cmd));
+    add_cmd(r, cmd_info("variables",    "declare new variables", variables_cmd));
+    add_cmd(r, cmd_info("parameters",   "declare new parameters", parameters_cmd));
+    add_cmd(r, cmd_info("constants",    "declare new constants (aka top-level variables)", constants_cmd));
     add_cmd(r, cmd_info("definition",   "add new definition", definition_cmd));
     add_cmd(r, cmd_info("opaque",       "add new opaque definition", opaque_definition_cmd));
     add_cmd(r, cmd_info("private",      "add new private definition/theorem", private_definition_cmd));
     add_cmd(r, cmd_info("protected",    "add new protected definition/theorem", protected_definition_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
-    add_cmd(r, cmd_info("variables",    "declare new parameters", variables_cmd));
 }
 }
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 289051add..be0b98bb2 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -80,7 +80,7 @@ void init_token_table(token_table & t) {
 
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",
-         "variables", "[persistent]", "[visible]", "[instance]",
+         "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible",
          "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import",
          "inductive", "record", "renaming", "extends", "structure", "module", "universe",
@@ -93,8 +93,7 @@ void init_token_table(token_table & t) {
          {g_qed_unicode, "qed"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
-        {{"parameter", "variable"}, {"parameters", "variables"}, {"lemma", "theorem"},
-         {"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"},
+        {{"lemma", "theorem"}, {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
          {nullptr, nullptr}};
 
     auto it = builtin;
diff --git a/tests/lean/alias.lean b/tests/lean/alias.lean
index 93c9db7dd..2e65ab64a 100644
--- a/tests/lean/alias.lean
+++ b/tests/lean/alias.lean
@@ -1,18 +1,18 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
-  variable foo : num → num → num
+  constant num : Type.{1}
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
-  variable foo : val → val → val
+  constant val : Type.{1}
+  constant foo : val → val → val
 end N2
 
 open N2
 open N1
-variables a b : num
+constants a b : num
 print raw foo a b
 open N2
 print raw foo a b
diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean
index 6ad8fdfa5..9f35ec34f 100644
--- a/tests/lean/bug1.lean
+++ b/tests/lean/bug1.lean
@@ -2,7 +2,7 @@ definition bool  : Type.{1}           := Type.{0}
 definition and   (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
 infixl `∧`:25 := and
 
-variable a : bool
+constant a : bool
 
 -- Error
 theorem and_intro (p q : bool) (H1 : p) (H2 : q) : a
diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean
index c784471f7..e019a57b0 100644
--- a/tests/lean/calc1.lean
+++ b/tests/lean/calc1.lean
@@ -1,11 +1,11 @@
-variable A : Type.{1}
+constant A : Type.{1}
 definition bool : Type.{1} := Type.{0}
-variable eq : A → A → bool
+constant eq : A → A → bool
 infixl `=`:50 := eq
 axiom subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b
 axiom eq_trans (a b c : A) (H1 : a = b) (H2 : b = c) : a = c
 axiom eq_refl (a : A) : a = a
-variable le : A → A → bool
+constant le : A → A → bool
 infixl `≤`:50 := le
 axiom le_trans (a b c : A) (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
 axiom le_refl (a : A) : a ≤ a
@@ -18,7 +18,7 @@ calc_trans eq_trans
 calc_trans le_trans
 calc_trans eq_le_trans
 calc_trans le_eq_trans
-variables a b c d e f : A
+constants a b c d e f : A
 axiom H1 : a = b
 axiom H2 : b ≤ c
 axiom H3 : c ≤ d
@@ -28,7 +28,7 @@ check calc a   = b : H1
            ... ≤ d : H3
            ... = e : H4
 
-variable lt : A → A → bool
+constant lt : A → A → bool
 infixl `<`:50 := lt
 axiom lt_trans (a b c : A) (H1 : a < b) (H2 : b < c) : a < c
 axiom le_lt_trans (a b c : A) (H1 : a ≤ b) (H2 : b < c) : a < c
@@ -40,9 +40,9 @@ calc_trans le_lt_trans
 check calc b  ≤ c : H2
           ... < d : H5
 
-variable le2 : A → A → bool
+constant le2 : A → A → bool
 infixl `≤`:50 := le2
-variable le2_trans (a b c : A) (H1 : le2 a b) (H2 : le2 b c) : le2 a c
+constant le2_trans (a b c : A) (H1 : le2 a b) (H2 : le2 b c) : le2 a c
 calc_trans le2_trans
 print raw calc b   ≤ c : H2
                ... ≤ d : H3
diff --git a/tests/lean/choice_expl.lean b/tests/lean/choice_expl.lean
index e06623b5c..3675652b8 100644
--- a/tests/lean/choice_expl.lean
+++ b/tests/lean/choice_expl.lean
@@ -7,8 +7,8 @@ namespace N2
 end N2
 
 open N1 N2
-variable N : Type.{1}
-variables a b : N
+constant N : Type.{1}
+constants a b : N
 check @pr
 check @pr N a b
 check pr a b
diff --git a/tests/lean/coe.lean b/tests/lean/coe.lean
index cacb825bd..758f8b098 100644
--- a/tests/lean/coe.lean
+++ b/tests/lean/coe.lean
@@ -8,5 +8,5 @@ mk : (Π (A B : Type), A → B) → Functor
 definition Functor.to_fun [coercion] (f : Functor) {A B : Type} : A → B :=
 Functor.rec (λ f, f) f A B
 
-variable f : Functor
+constant f : Functor
 check f 0 = 0
diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean
index 2fe4534b1..30444a016 100644
--- a/tests/lean/have1.lean
+++ b/tests/lean/have1.lean
@@ -1,7 +1,7 @@
 import logic
 open bool eq.ops tactic eq
 
-variables a b c : bool
+constants a b c : bool
 axiom H1 : a = b
 axiom H2 : b = c
 
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index b7008e20f..5a44e453b 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -8,7 +8,7 @@ mk : A → C A
 definition val {A : Type} (c : C A) : A :=
 C.rec (λa, a) c
 
-variable magic (A : Type) : A
+constant magic (A : Type) : A
 definition C_magic [instance] [priority max] (A : Type) : C A :=
 C.mk (magic A)
 
diff --git a/tests/lean/interactive/coe.lean b/tests/lean/interactive/coe.lean
index 901f969c7..a305ab32d 100644
--- a/tests/lean/interactive/coe.lean
+++ b/tests/lean/interactive/coe.lean
@@ -4,6 +4,6 @@ open int
 protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
 take (a b : ℤ), _
 
-variable n : nat
-variable i : int
+constant n : nat
+constant i : int
 check n + i
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index d49dee2eb..58b36b4d0 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,7 +1,7 @@
 import data.num
 
 
-variable f : num → num → num → num
+constant f : num → num → num → num
 
 check
   let a := 10
diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean
index 1e26fc6f5..342198cc2 100644
--- a/tests/lean/let4.lean
+++ b/tests/lean/let4.lean
@@ -1,7 +1,7 @@
 import data.num
 
 
-variable f : num → num → num → num
+constant f : num → num → num → num
 
 check
   let a := 10,
diff --git a/tests/lean/num2.lean b/tests/lean/num2.lean
index 873706673..2516627d7 100644
--- a/tests/lean/num2.lean
+++ b/tests/lean/num2.lean
@@ -1,12 +1,12 @@
 set_option pp.notation false
 definition Prop := Type.{0}
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infixl `=`:50 := eq
 
-variable N : Type.{1}
-variable z : N
-variable o : N
-variable b : N
+constant N : Type.{1}
+constant z : N
+constant o : N
+constant b : N
 
 notation 0 := z
 notation 1 := o
@@ -14,9 +14,9 @@ notation 1 := o
 check 1
 check 0
 
-variable G : Type.{1}
-variable gz : G
-variable a  : G
+constant G : Type.{1}
+constant gz : G
+constant a  : G
 
 notation 0 := gz
 
diff --git a/tests/lean/num3.lean b/tests/lean/num3.lean
index 5241cbcc6..bba618b98 100644
--- a/tests/lean/num3.lean
+++ b/tests/lean/num3.lean
@@ -2,10 +2,10 @@ import data.num
 set_option pp.notation false
 set_option pp.implicit true
 
-variable N : Type.{1}
-variable z : N
-variable o : N
-variable a : N
+constant N : Type.{1}
+constant z : N
+constant o : N
+constant a : N
 
 notation 0 := z
 notation 1 := o
diff --git a/tests/lean/num4.lean b/tests/lean/num4.lean
index 9955cc8c3..f5fd4d670 100644
--- a/tests/lean/num4.lean
+++ b/tests/lean/num4.lean
@@ -3,10 +3,10 @@ set_option pp.notation false
 set_option pp.implicit true
 
 namespace foo
-  variable N : Type.{1}
-  variable z : N
-  variable o : N
-  variable a : N
+  constant N : Type.{1}
+  constant z : N
+  constant o : N
+  constant a : N
   notation 0 := z
   notation 1 := o
 
diff --git a/tests/lean/run/abs.lean b/tests/lean/run/abs.lean
index 9c9b9d1ef..2654a18a2 100644
--- a/tests/lean/run/abs.lean
+++ b/tests/lean/run/abs.lean
@@ -1,7 +1,7 @@
 import data.int
 open int
 
-variable abs : int → int
+constant abs : int → int
 notation `|`:40 A:40 `|` := abs A
-variables a b c : int
+constants a b c : int
 check |a + |b| + c|
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 89d7cd01c..32f5c3b46 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -38,8 +38,8 @@ end algebra
 
 namespace nat
 
-  variable add : nat → nat → nat
-  variable mul : nat → nat → nat
+  constant add : nat → nat → nat
+  constant mul : nat → nat → nat
 
   definition is_mul_struct  [instance] : algebra.mul_struct nat
   := algebra.mul_struct.mk mul
@@ -105,8 +105,8 @@ end algebra
 
 section
   open algebra algebra.semigroup algebra.monoid
-  variable M : monoid
-  variables a b c : M
+  parameter M : monoid
+  parameters a b c : M
   check a*b*c*a*b*c*a*b*a*b*c*a
   check a*b
 end
diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean
index 4aa8a7c8f..1ceed6318 100644
--- a/tests/lean/run/alias1.lean
+++ b/tests/lean/run/alias1.lean
@@ -1,25 +1,25 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
-  variable foo : num → num → num
+  constant num : Type.{1}
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
-  variable foo : val → val → val
+  constant val : Type.{1}
+  constant foo : val → val → val
 end N2
 
 open N1
 open N2
-variables a b : num
-variables x y : val
+constants a b : num
+constants x y : val
 
 
 check foo a b
 check foo x y
 
-variable f : num → val
+constant f : num → val
 coercion f
 
 check foo a x
diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean
index aec611e39..545ec6c47 100644
--- a/tests/lean/run/alias2.lean
+++ b/tests/lean/run/alias2.lean
@@ -1,19 +1,19 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
-  variable foo : num → num → num
+  constant num : Type.{1}
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
-  variable foo : val → val → val
+  constant val : Type.{1}
+  constant foo : val → val → val
 end N2
 
 open N1
 open N2
-variables a b : num
-variable f : num → val
+constants a b : num
+constant f : num → val
 coercion f
 
 definition aux2 := foo a b
diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean
index 48e3d6825..9cc7744f2 100644
--- a/tests/lean/run/alias3.lean
+++ b/tests/lean/run/alias3.lean
@@ -3,7 +3,7 @@ import logic
 namespace N1
   section
     section
-      variable A : Type
+      parameter A : Type
       definition foo (a : A) : Prop := true
       check foo
     end
diff --git a/tests/lean/run/basic.lean b/tests/lean/run/basic.lean
index d23959a23..e57cc611c 100644
--- a/tests/lean/run/basic.lean
+++ b/tests/lean/run/basic.lean
@@ -1,9 +1,9 @@
-variable A.{l1 l2} : Type.{l1} → Type.{l2}
+constant A.{l1 l2} : Type.{l1} → Type.{l2}
 check A
 definition tst.{l} (A : Type) (B : Type) (C : Type.{l}) : Type := A → B → C
 check tst
-variable group.{l} : Type.{l+1}
-variable carrier.{l} : group.{l} → Type.{l}
+constant group.{l} : Type.{l+1}
+constant carrier.{l} : group.{l} → Type.{l}
 definition to_carrier (g : group) := carrier g
 
 check to_carrier.{1}
@@ -13,11 +13,11 @@ section
   check A
   definition B := A → A
 end
-variable N : Type.{1}
+constant N : Type.{1}
 check B N
-variable f : B N
+constant f : B N
 check f
-variable a : N
+constant a : N
 check f a
 
 section
@@ -31,7 +31,7 @@ check double
 check double.{1 2}
 
 definition Prop := Type.{0}
-variable eq : Π {A : Type}, A → A → Prop
+constant eq : Π {A : Type}, A → A → Prop
 infix `=`:50 := eq
 
 check eq.{1}
diff --git a/tests/lean/run/bug6.lean b/tests/lean/run/bug6.lean
index 73943ac54..75a176dff 100644
--- a/tests/lean/run/bug6.lean
+++ b/tests/lean/run/bug6.lean
@@ -4,8 +4,8 @@ section
   parameter {A : Type}
   theorem T {a b : A} (H : a = b) : b = a
   := symm H
-  variables x y : A
-  axiom H : x = y
+  parameters x y : A
+  hypothesis H : x = y
   check T H
   check T
 end
@@ -14,8 +14,8 @@ section
   parameter {A : Type}
   theorem T2 ⦃a b : A⦄ (H : a = b) : b = a
   := symm H
-  variables x y : A
-  axiom H : x = y
+  parameters x y : A
+  hypothesis H : x = y
   check T2 H
   check T2
 end
diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean
index 90b57ee67..dbc6f286e 100644
--- a/tests/lean/run/calc.lean
+++ b/tests/lean/run/calc.lean
@@ -2,7 +2,7 @@ import data.num
 
 
 namespace foo
-  variable le : num → num → Prop
+  constant le : num → num → Prop
   axiom le_trans {a b c : num} : le a b → le b c → le a c
   calc_trans le_trans
   infix `≤`:50 := le
diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean
index 1784d6a3d..3dc8f54d7 100644
--- a/tests/lean/run/class11.lean
+++ b/tests/lean/run/class11.lean
@@ -1,9 +1,9 @@
 import logic
 
-variable C {A : Type} : A → Prop
+constant C {A : Type} : A → Prop
 class C
 
-variable f {A : Type} (a : A) {H : C a} : Prop
+constant f {A : Type} (a : A) {H : C a} : Prop
 
 definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop :=
 f a ∧ f b
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 1cc16a2a0..cf0aac9bf 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -68,9 +68,9 @@ theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x
 theorem not_zero_succ [instance] (x : nat) : not_zero (succ x)
 := not_zero.intro (not_is_zero_succ x)
 
-variable dvd : Π (x y : nat) {H : not_zero y}, nat
+constant dvd : Π (x y : nat) {H : not_zero y}, nat
 
-variables a b : nat
+constants a b : nat
 
 set_option pp.implicit true
 reducible add
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index 13df8edef..6615364c6 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -15,8 +15,8 @@ namespace nat
   zero : nat,
   succ : nat → nat
 
-  variable mul : nat → nat → nat
-  variable add : nat → nat → nat
+  constant mul : nat → nat → nat
+  constant add : nat → nat → nat
 
   definition mul_struct [instance] : algebra.mul_struct nat
   := algebra.mul_struct.mk mul
@@ -24,7 +24,7 @@ end nat
 
 section
   open algebra nat
-  variables a b c : nat
+  parameters a b c : nat
   check a * b * c
   definition tst1 : nat := a * b * c
 end
@@ -33,7 +33,7 @@ section
   open [notation] algebra
   open nat
   -- check mul_struct nat  << This is an error, we are open only the notation from algebra
-  variables a b c : nat
+  parameters a b c : nat
   check a * b * c
   definition tst2 : nat := a * b * c
 end
@@ -41,7 +41,7 @@ end
 section
   open nat
   -- check mul_struct nat  << This is an error, we are open only the notation from algebra
-  variables a b c : nat
+  parameters a b c : nat
   check #algebra a*b*c
   definition tst3 : nat := #algebra a*b*c
 end
@@ -52,7 +52,7 @@ section
   definition add_struct [instance] : algebra.mul_struct nat
   := algebra.mul_struct.mk add
 
-  variables a b c : nat
+  parameters a b c : nat
   check #algebra a*b*c  -- << is open add instead of mul
   definition tst4 : nat := #algebra a*b*c
 end
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index b5ede50a2..b4b28638d 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -1,10 +1,10 @@
 import data.num
 
 
-variables int nat real : Type.{1}
-variable nat_add  : nat → nat → nat
-variable int_add  : int → int → int
-variable real_add : real → real → real
+constants int nat real : Type.{1}
+constant nat_add  : nat → nat → nat
+constant int_add  : int → int → int
+constant real_add : real → real → real
 
 inductive add_struct (A : Type) :=
 mk : (A → A → A) → add_struct A
@@ -18,12 +18,12 @@ definition add_nat_struct  [instance] : add_struct nat := add_struct.mk nat_add
 definition add_int_struct  [instance] : add_struct int := add_struct.mk int_add
 definition add_real_struct [instance] : add_struct real := add_struct.mk real_add
 
-variables n m : nat
-variables i j : int
-variables x y : real
-variable num_to_nat : num → nat
-variable nat_to_int : nat → int
-variable int_to_real : int → real
+constants n m : nat
+constants i j : int
+constants x y : real
+constant num_to_nat : num → nat
+constant nat_to_int : nat → int
+constant int_to_real : int → real
 coercion num_to_nat
 coercion nat_to_int
 coercion int_to_real
@@ -47,7 +47,7 @@ check i + 0
 check 0 + x
 check x + 0
 namespace foo
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infixl `=`:50 := eq
 definition id (A : Type) (a : A) := a
 notation A `=` B `:` C := @eq C A B
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
index 3b42849ce..7c5596b80 100644
--- a/tests/lean/run/coe1.lean
+++ b/tests/lean/run/coe1.lean
@@ -1,15 +1,15 @@
-variable A : Type.{1}
-variable B : Type.{1}
-variable f : A → B
+constant A : Type.{1}
+constant B : Type.{1}
+constant f : A → B
 coercion f
-variable g : B → B → B
-variables a1 a2 a3 : A
-variables b1 b2 b3 : B
+constant g : B → B → B
+constants a1 a2 a3 : A
+constants b1 b2 b3 : B
 check g a1 b1
 set_option pp.coercions true
 check g a1 b1
 
-variable eq {A : Type} : A → A → Type.{0}
+constant eq {A : Type} : A → A → Type.{0}
 check eq a1 a2
 check eq a1 b1
 set_option pp.implicit true
diff --git a/tests/lean/run/coe10.lean b/tests/lean/run/coe10.lean
index 28330219f..cf3101b31 100644
--- a/tests/lean/run/coe10.lean
+++ b/tests/lean/run/coe10.lean
@@ -10,8 +10,8 @@ fn2.rec (λ f g, f) f
 definition to_bc [coercion] {A B C : Type} (f : fn2 A B C) : B → C :=
 fn2.rec (λ f g, g) f
 
-variable f : fn2 Prop nat nat
-variable a : Prop
-variable n : nat
+constant f : fn2 Prop nat nat
+constant a : Prop
+constant n : nat
 check f a
 check f n
diff --git a/tests/lean/run/coe11.lean b/tests/lean/run/coe11.lean
index e6a4023cb..72e8fe87c 100644
--- a/tests/lean/run/coe11.lean
+++ b/tests/lean/run/coe11.lean
@@ -14,12 +14,12 @@ definition my_morphism [coercion] {obC obD : Type} {C : category obC} {D : categ
       Π{A B : obC}, mor A B → mor (my_object F A) (my_object F B) :=
 my_functor.rec (λ obF morF Hid Hcomp, morF) F
 
-variables obC obD : Type
-variables a b : obC
-variable C : category obC
+constants obC obD : Type
+constants a b : obC
+constant C : category obC
 instance C
-variable D : category obD
-variable F : my_functor C D
-variable m : mor a b
+constant D : category obD
+constant F : my_functor C D
+constant m : mor a b
 check F a
 check F m
diff --git a/tests/lean/run/coe12.lean b/tests/lean/run/coe12.lean
index 5a81051a9..0bf4b9ac8 100644
--- a/tests/lean/run/coe12.lean
+++ b/tests/lean/run/coe12.lean
@@ -5,6 +5,6 @@ mk : (Π {C : Type}, A → C → B) → foo A B
 definition to_fun [coercion] {A B : Type} (f : foo A B) : Π {C : Type}, A → C → B :=
 foo.rec (λf, f) f
 
-variable f : foo nat nat
-variable a : nat
+constant f : foo nat nat
+constant a : nat
 check f a true
diff --git a/tests/lean/run/coe13.lean b/tests/lean/run/coe13.lean
index 98c159623..90a559081 100644
--- a/tests/lean/run/coe13.lean
+++ b/tests/lean/run/coe13.lean
@@ -15,7 +15,7 @@ struct.rec (λA r, A) s
 
 definition g (f : nat → nat) (a : nat) := f a
 
-variable f : functor nat nat
+constant f : functor nat nat
 
 check g (functor.to_fun f) 0
 
@@ -23,8 +23,8 @@ check g f 0
 
 definition id (A : Type) (a : A) := a
 
-variable S : struct
-variable a : S
+constant S : struct
+constant a : S
 
 check id (struct.to_sort S) a
 check id S a
diff --git a/tests/lean/run/coe14.lean b/tests/lean/run/coe14.lean
index 98c159623..90a559081 100644
--- a/tests/lean/run/coe14.lean
+++ b/tests/lean/run/coe14.lean
@@ -15,7 +15,7 @@ struct.rec (λA r, A) s
 
 definition g (f : nat → nat) (a : nat) := f a
 
-variable f : functor nat nat
+constant f : functor nat nat
 
 check g (functor.to_fun f) 0
 
@@ -23,8 +23,8 @@ check g f 0
 
 definition id (A : Type) (a : A) := a
 
-variable S : struct
-variable a : S
+constant S : struct
+constant a : S
 
 check id (struct.to_sort S) a
 check id S a
diff --git a/tests/lean/run/coe6.lean b/tests/lean/run/coe6.lean
index 2c3af9f22..66fa38f99 100644
--- a/tests/lean/run/coe6.lean
+++ b/tests/lean/run/coe6.lean
@@ -1,12 +1,12 @@
 import data.unit
 open unit
 
-variable int : Type.{1}
-variable nat : Type.{1}
-variable izero : int
-variable nzero : nat
-variable isucc : int → int
-variable nsucc : nat → nat
+constant int : Type.{1}
+constant nat : Type.{1}
+constant izero : int
+constant nzero : nat
+constant isucc : int → int
+constant nsucc : nat → nat
 definition f [coercion] (a : unit) : int := izero
 definition g [coercion] (a : unit) : nat := nzero
 
diff --git a/tests/lean/run/coe7.lean b/tests/lean/run/coe7.lean
index f6caa150d..7e04f300b 100644
--- a/tests/lean/run/coe7.lean
+++ b/tests/lean/run/coe7.lean
@@ -1,8 +1,8 @@
 import logic
 
-variable nat : Type.{1}
-variable int : Type.{1}
-variable of_nat : nat → int
+constant nat : Type.{1}
+constant int : Type.{1}
+constant of_nat : nat → int
 coercion of_nat
 
 theorem tst (n : nat) : n = n :=
diff --git a/tests/lean/run/coe8.lean b/tests/lean/run/coe8.lean
index 93b8c2da0..bb8e3f218 100644
--- a/tests/lean/run/coe8.lean
+++ b/tests/lean/run/coe8.lean
@@ -1,16 +1,16 @@
 import logic
 
-variable nat : Type.{1}
-variable int : Type.{1}
-variable of_nat : nat → int
+constant nat : Type.{1}
+constant int : Type.{1}
+constant of_nat : nat → int
 coercion of_nat
-variable nat_add : nat → nat → nat
-variable int_add : int → int → int
+constant nat_add : nat → nat → nat
+constant int_add : int → int → int
 infixl `+`:65 := int_add
 infixl `+`:65 := nat_add
 
 print "================"
-variable tst (n m : nat) : @eq int (of_nat n + of_nat m) (n + m)
+constant tst (n m : nat) : @eq int (of_nat n + of_nat m) (n + m)
 
 check tst
 exit
diff --git a/tests/lean/run/coe9.lean b/tests/lean/run/coe9.lean
index 9c16af0d7..d0867e25e 100644
--- a/tests/lean/run/coe9.lean
+++ b/tests/lean/run/coe9.lean
@@ -1,25 +1,25 @@
 import data.nat
 open nat
 
-variable list.{l} : Type.{l} → Type.{l}
-variable vector.{l} : Type.{l} → nat → Type.{l}
-variable matrix.{l} : Type.{l} → nat → nat → Type.{l}
-variable length : Pi {A : Type}, list A → nat
+constant list.{l} : Type.{l} → Type.{l}
+constant vector.{l} : Type.{l} → nat → Type.{l}
+constant matrix.{l} : Type.{l} → nat → nat → Type.{l}
+constant length : Pi {A : Type}, list A → nat
 
-variable list_to_vec {A : Type} (l : list A) : vector A (length l)
-variable to_row {A : Type} {n : nat} : vector A n → matrix A 1 n
-variable to_col {A : Type} {n : nat} : vector A n → matrix A n 1
-variable to_list {A : Type} {n : nat} : vector A n → list A
+constant list_to_vec {A : Type} (l : list A) : vector A (length l)
+constant to_row {A : Type} {n : nat} : vector A n → matrix A 1 n
+constant to_col {A : Type} {n : nat} : vector A n → matrix A n 1
+constant to_list {A : Type} {n : nat} : vector A n → list A
 
 coercion to_row
 coercion to_col
 coercion list_to_vec
 coercion to_list
 
-variable f {A : Type} {n : nat} (M : matrix A n 1) : nat
-variable g {A : Type} {n : nat} (M : matrix A 1 n) : nat
-variable v : vector nat 10
-variable l : list nat
+constant f {A : Type} {n : nat} (M : matrix A n 1) : nat
+constant g {A : Type} {n : nat} (M : matrix A 1 n) : nat
+constant v : vector nat 10
+constant l : list nat
 
 check f v
 check g v
diff --git a/tests/lean/run/coefun.lean b/tests/lean/run/coefun.lean
index eca7730b7..78c9ca7cf 100644
--- a/tests/lean/run/coefun.lean
+++ b/tests/lean/run/coefun.lean
@@ -7,7 +7,7 @@ mk : (obj A → obj B) → fn A B
 definition to_fun [coercion] {A B : Type} (f : fn A B) : obj A → obj B :=
 fn.rec (λf, f) f
 
-variable n : Type.{1}
-variable f : fn n n
-variable a : obj n
+constant n : Type.{1}
+constant f : fn n n
+constant a : obj n
 check (f a)
diff --git a/tests/lean/run/ctx.lean b/tests/lean/run/ctx.lean
index 0d2af9f1f..ec2a83049 100644
--- a/tests/lean/run/ctx.lean
+++ b/tests/lean/run/ctx.lean
@@ -1,8 +1,8 @@
 import data.nat logic.core.inhabited
 open nat inhabited
 
-variable N : Type.{1}
-variable a : N
+constant N : Type.{1}
+constant a : N
 
 section s1
   set_option pp.implicit true
@@ -18,5 +18,5 @@ section s1
 end s1
 
 theorem tst : inhabited nat
-variables n m : nat
+constants n m : nat
 check n = a
diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean
index 2373d80cc..bf04e8e55 100644
--- a/tests/lean/run/decidable.lean
+++ b/tests/lean/run/decidable.lean
@@ -1,7 +1,7 @@
 import logic data.unit
 open bool unit decidable
 
-variables a b c : bool
-variables u v : unit
+constants a b c : bool
+constants u v : unit
 set_option pp.implicit true
 check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = tt ↔ true) then a else b
diff --git a/tests/lean/run/e1.lean b/tests/lean/run/e1.lean
index 7f2a97b99..889a2d8d1 100644
--- a/tests/lean/run/e1.lean
+++ b/tests/lean/run/e1.lean
@@ -1,15 +1,15 @@
 definition Prop : Type.{1} := Type.{0}
-variable eq : forall {A : Type}, A → A → Prop
-variable N : Type.{1}
-variables a b c : N
+constant eq : forall {A : Type}, A → A → Prop
+constant N : Type.{1}
+constants a b c : N
 infix `=`:50 := eq
 check a = b
 
-variable f : Prop → N → N
-variable g : N → N → N
+constant f : Prop → N → N
+constant g : N → N → N
 precedence `+`:50
 infixl + := f
 infixl + := g
 check a + b + c
-variable p : Prop
+constant p : Prop
 check p + a + b + c
diff --git a/tests/lean/run/e10.lean b/tests/lean/run/e10.lean
index 5a324f3db..a44ada2b6 100644
--- a/tests/lean/run/e10.lean
+++ b/tests/lean/run/e10.lean
@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
@@ -19,8 +19,8 @@ section
   open nat
   open int
 
-  variables n m : nat
-  variables i j : int
+  parameters n m : nat
+  parameters i j : int
 
   -- 'Most recent' are always tried first
   print raw i + n
@@ -41,5 +41,5 @@ section
 end
 
 
-variables a b : nat.nat
+constants a b : nat.nat
 check #nat a + b
diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index d3e29926c..5a2fa9194 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
@@ -22,8 +22,8 @@ section
   open [decls] nat
   open [decls] int
 
-  variables n m : nat
-  variables i j : int
+  parameters n m : nat
+  parameters i j : int
   check n + m
   check i + j
 
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index 33106d30f..0d3bb20b8 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -1,22 +1,22 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
-variables n m : nat.nat
-variables i j : int.int
+constants n m : nat.nat
+constants i j : int.int
 
 section
   open [notation] nat
diff --git a/tests/lean/run/e13.lean b/tests/lean/run/e13.lean
index cfa00463f..492208db0 100644
--- a/tests/lean/run/e13.lean
+++ b/tests/lean/run/e13.lean
@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   namespace coercions
     coercion of_nat
   end coercions
@@ -19,7 +19,7 @@ end int
 
 open nat
 open int
-variables n m : nat
+constants n m : nat
 check n+m -- coercion nat -> int is not available
 open int.coercions
 check n+m -- coercion nat -> int is available
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index 62af072d6..a9aae9ac9 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -22,7 +22,7 @@ vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
-variable n : nat
+constant n : nat
 check vcons n vnil
 
 check vector.rec
@@ -32,7 +32,7 @@ definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
 
 coercion vector_to_list
 
-variable f : forall {A : Type}, list A → nat
+constant f : forall {A : Type}, list A → nat
 
 check f (cons zero nil)
 check f (vcons zero vnil)
diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean
index cbc0d1727..2ec9eec2b 100644
--- a/tests/lean/run/e15.lean
+++ b/tests/lean/run/e15.lean
@@ -20,7 +20,7 @@ vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
-variable n : nat
+constant n : nat
 check vcons n vnil
 
 check vector.rec
diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean
index a28e4ea52..9cc1134d7 100644
--- a/tests/lean/run/e16.lean
+++ b/tests/lean/run/e16.lean
@@ -21,7 +21,7 @@ vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
-variable n : nat
+constant n : nat
 check vcons n vnil
 
 check vector.rec
diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean
index 7fe86e4e0..7835b23db 100644
--- a/tests/lean/run/e17.lean
+++ b/tests/lean/run/e17.lean
@@ -12,8 +12,8 @@ neg : nat → int
 
 coercion int.of_nat
 
-variables n m : nat
-variables i j : int
+constants n m : nat
+constants i j : int
 namespace list end list open list
 
 check cons i (cons i nil)
diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
index 1ab4026c1..82174ed3d 100644
--- a/tests/lean/run/e18.lean
+++ b/tests/lean/run/e18.lean
@@ -12,9 +12,9 @@ neg : nat → int
 
 coercion int.of_nat
 
-variables n m : nat
-variables i j : int
-variable l : list nat
+constants n m : nat
+constants i j : int
+constant l : list nat
 namespace list end list open list
 
 check cons i (cons i nil)
diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean
index 65097cec7..32b97e4b6 100644
--- a/tests/lean/run/e5.lean
+++ b/tests/lean/run/e5.lean
@@ -40,7 +40,7 @@ print "using strict implicit arguments"
 definition symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a
 
 check symmetric
-variable p : nat → nat → Prop
+constant p : nat → nat → Prop
 check symmetric p
 axiom H1 : symmetric p
 axiom H2 : p zero (succ zero)
diff --git a/tests/lean/run/e6.lean b/tests/lean/run/e6.lean
index a990e04d2..1e456483e 100644
--- a/tests/lean/run/e6.lean
+++ b/tests/lean/run/e6.lean
@@ -1,25 +1,25 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
 open int
 open nat
 
-variables n m : nat
-variables i j : int
+constants n m : nat
+constants i j : int
 
 check n + m
 check i + j
diff --git a/tests/lean/run/e7.lean b/tests/lean/run/e7.lean
index 042d4f995..13310fd8c 100644
--- a/tests/lean/run/e7.lean
+++ b/tests/lean/run/e7.lean
@@ -1,25 +1,25 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
 open nat
 open int
 
-variables n m : nat
-variables i j : int
+constants n m : nat
+constants i j : int
 
 -- 'Most recent' are always tried first
 print raw i + n
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index 852877e99..73f1e2382 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
   coercion of_nat
 end int
 
@@ -21,8 +21,8 @@ open [notation] int
 open [decls] nat
 open [decls] int
 
-variables n m : nat
-variables i j : int
+constants n m : nat
+constants i j : int
 check n + m
 check i + j
 
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
index 5b585020a..48fbb3162 100644
--- a/tests/lean/run/e9.lean
+++ b/tests/lean/run/e9.lean
@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
-  variable add : nat → nat → nat
+  constant nat : Type.{1}
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
-  variable add : int → int → int
+  constant int : Type.{1}
+  constant add : int → int → int
   infixl + := add
-  variable of_nat : nat → int
+  constant of_nat : nat → int
 end int
 
 namespace int_coercions
@@ -22,8 +22,8 @@ end int_coercions
 open nat
 open int
 
-variables n m : nat
-variables i j : int
+constants n m : nat
+constants i j : int
 check n + m
 check i + j
 
diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean
index 896926d02..ab8e2e29f 100644
--- a/tests/lean/run/elim.lean
+++ b/tests/lean/run/elim.lean
@@ -1,6 +1,6 @@
 import logic
 
-variable p : num → num → num → Prop
+constant p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
 axiom H2 : ∀ {x y z : num}, p x y z → p x x x
 theorem tst : ∃ x, p x x x
diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean
index c1a2e677c..7d51cf1a5 100644
--- a/tests/lean/run/elim2.lean
+++ b/tests/lean/run/elim2.lean
@@ -1,6 +1,6 @@
 import logic
 open tactic
-variable p : num → num → num → Prop
+constant p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
 axiom H2 : ∀ {x y z : num}, p x y z → p x x x
 theorem tst : ∃ x, p x x x
diff --git a/tests/lean/run/export.lean b/tests/lean/run/export.lean
index 623541ac5..7983c99a6 100644
--- a/tests/lean/run/export.lean
+++ b/tests/lean/run/export.lean
@@ -1,6 +1,6 @@
 import data.nat
 
-variables a b : nat
+constants a b : nat
 
 namespace boo
   export nat (rec add)
diff --git a/tests/lean/run/full.lean b/tests/lean/run/full.lean
index 63a5580ba..c12376659 100644
--- a/tests/lean/run/full.lean
+++ b/tests/lean/run/full.lean
@@ -1,6 +1,6 @@
 import logic
 namespace foo
-  variable x : num
+  constant x : num
   check x
   check x
   set_option pp.full_names true
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 689e5be04..a602b6cd0 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -2,22 +2,22 @@ import logic algebra.function
 open function bool
 
 
-variable f : num → bool
-variable g : num → num
+constant f : num → bool
+constant g : num → num
 
 check f ∘ g ∘ g
 
 check typeof id : num → num
 check num → num ⟨is_typeof⟩ id
 
-variable h : num → bool → num
+constant h : num → bool → num
 
 check flip h
 check flip h ff num.zero
 
 check typeof flip h ff num.zero : num
 
-variable f1 : num → num → bool
-variable f2 : bool → num
+constant f1 : num → num → bool
+constant f2 : bool → num
 
 check (f1 on f2) ff tt
diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean
index 4fd03f33a..ac1dcac07 100644
--- a/tests/lean/run/group.lean
+++ b/tests/lean/run/group.lean
@@ -31,9 +31,9 @@ definition mul {A : Type} {s : group_struct A} (a b : A) : A
 
 infixl `*`:75 := mul
 
-variable  G1 : group.{1}
-variable  G2 : group.{1}
-variables a b c : (carrier G2)
-variables d e : (carrier G1)
+constant  G1 : group.{1}
+constant  G2 : group.{1}
+constants a b c : (carrier G2)
+constants d e : (carrier G1)
 check a * b * b
 check d * e
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index db7792c78..ed5b941f4 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -34,23 +34,23 @@ definition mul {A : Type} {s : group_struct A} (a b : A) : A
 infixl `*`:75 := mul
 
 section
-  variable  G1 : group
-  variable  G2 : group
-  variables a b c : G2
-  variables d e   : G1
+  parameter  G1 : group
+  parameter  G2 : group
+  parameters a b c : G2
+  parameters d e   : G1
   check a * b * b
   check d * e
 end
 
-variable G : group.{1}
-variables a b : G
+constant G : group.{1}
+constants a b : G
 definition val : G := a*b
 check val
 
-variable pos_real : Type.{1}
-variable rmul  : pos_real → pos_real → pos_real
-variable rone  : pos_real
-variable rinv  : pos_real → pos_real
+constant pos_real : Type.{1}
+constant rmul  : pos_real → pos_real → pos_real
+constant rone  : pos_real
+constant rinv  : pos_real → pos_real
 axiom    H1    : is_assoc rmul
 axiom    H2    : is_id rmul rone
 axiom    H3    : is_inv rmul rone rinv
@@ -58,7 +58,7 @@ axiom    H3    : is_inv rmul rone rinv
 definition real_group_struct [instance] : group_struct pos_real
 := group_struct.mk rmul rone rinv H1 H2 H3
 
-variables x y : pos_real
+constants x y : pos_real
 check x * y
 set_option pp.implicit true
 print "---------------"
diff --git a/tests/lean/run/have1.lean b/tests/lean/run/have1.lean
index c75858e6a..be42f602c 100644
--- a/tests/lean/run/have1.lean
+++ b/tests/lean/run/have1.lean
@@ -1,5 +1,5 @@
 definition Prop : Type.{1} := Type.{0}
-variables a b c : Prop
+constants a b c : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/have2.lean b/tests/lean/run/have2.lean
index 8e9715277..1f55029bf 100644
--- a/tests/lean/run/have2.lean
+++ b/tests/lean/run/have2.lean
@@ -1,5 +1,5 @@
 definition Prop : Type.{1} := Type.{0}
-variables a b c : Prop
+constants a b c : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/have3.lean b/tests/lean/run/have3.lean
index d0dbf963b..5e0b6a95d 100644
--- a/tests/lean/run/have3.lean
+++ b/tests/lean/run/have3.lean
@@ -1,5 +1,5 @@
 definition Prop : Type.{1} := Type.{0}
-variables a b c : Prop
+constants a b c : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/have4.lean b/tests/lean/run/have4.lean
index 5fc4eb2be..1c23eff0b 100644
--- a/tests/lean/run/have4.lean
+++ b/tests/lean/run/have4.lean
@@ -1,5 +1,5 @@
 definition Prop : Type.{1} := Type.{0}
-variables a b c : Prop
+constants a b c : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/have5.lean b/tests/lean/run/have5.lean
index 4120df3b9..1046f8766 100644
--- a/tests/lean/run/have5.lean
+++ b/tests/lean/run/have5.lean
@@ -1,6 +1,6 @@
 import logic
 open tactic
-variables a b c d : Prop
+constants a b c d : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/have6.lean b/tests/lean/run/have6.lean
index d05d03f43..ea3ca93dc 100644
--- a/tests/lean/run/have6.lean
+++ b/tests/lean/run/have6.lean
@@ -1,8 +1,8 @@
 definition Prop : Type.{1} := Type.{0}
-variable and : Prop → Prop → Prop
+constant and : Prop → Prop → Prop
 infixl `∧`:25 := and
-variable and_intro : forall (a b : Prop), a → b → a ∧ b
-variables a b c d : Prop
+constant and_intro : forall (a b : Prop), a → b → a ∧ b
+constants a b c d : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c
diff --git a/tests/lean/run/imp.lean b/tests/lean/run/imp.lean
index 35a43b52f..0a9721f68 100644
--- a/tests/lean/run/imp.lean
+++ b/tests/lean/run/imp.lean
@@ -1,6 +1,6 @@
-variable N : Type.{1}
-variables a b c : N
-variable f : forall {a b : N}, N → N
+constant N : Type.{1}
+constants a b c : N
+constant f : forall {a b : N}, N → N
 
 check f
 check @f
@@ -13,7 +13,7 @@ definition l2 : N → N → N := @f a
 definition l3 : N → N := @f a b
 definition l4 : N := @f a b c
 
-variable g : forall ⦃a b : N⦄, N → N
+constant g : forall ⦃a b : N⦄, N → N
 
 check g
 check g a
diff --git a/tests/lean/run/impbug1.lean b/tests/lean/run/impbug1.lean
index 388ec6658..5a2789f8c 100644
--- a/tests/lean/run/impbug1.lean
+++ b/tests/lean/run/impbug1.lean
@@ -1,7 +1,7 @@
 -- category
 
 definition Prop := Type.{0}
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infix `=`:50 := eq
 
 inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
diff --git a/tests/lean/run/impbug2.lean b/tests/lean/run/impbug2.lean
index 23761ead6..66f2dccfb 100644
--- a/tests/lean/run/impbug2.lean
+++ b/tests/lean/run/impbug2.lean
@@ -1,7 +1,7 @@
 -- category
 
 definition Prop := Type.{0}
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infix `=`:50 := eq
 
 inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
@@ -9,9 +9,9 @@ mk : Π (id : Π (A : ob), mor A A),
      (Π (A B : ob) (f : mor A A), id A = f) → category ob mor
 
 definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
-variable ob  : Type.{1}
-variable mor : ob → ob → Type.{1}
-variable Cat : category ob mor
+constant ob  : Type.{1}
+constant mor : ob → ob → Type.{1}
+constant Cat : category ob mor
 
 theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f :=
 @category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
diff --git a/tests/lean/run/impbug3.lean b/tests/lean/run/impbug3.lean
index c118563e8..5c9eb720a 100644
--- a/tests/lean/run/impbug3.lean
+++ b/tests/lean/run/impbug3.lean
@@ -1,18 +1,18 @@
 -- category
 
 definition Prop := Type.{0}
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infix `=`:50 := eq
 
-variable ob  : Type.{1}
-variable mor : ob → ob → Type.{1}
+constant ob  : Type.{1}
+constant mor : ob → ob → Type.{1}
 
 inductive category : Type :=
 mk : Π (id : Π (A : ob), mor A A),
      (Π (A B : ob) (f : mor A A), id A = f) → category
 
 definition id (Cat : category) := category.rec (λ id idl, id) Cat
-variable Cat : category
+constant Cat : category
 
 theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
 @category.rec (λ (C : category), @eq (mor A A) (id C A) f)
diff --git a/tests/lean/run/impbug4.lean b/tests/lean/run/impbug4.lean
index a01b0b39a..a4fcd6334 100644
--- a/tests/lean/run/impbug4.lean
+++ b/tests/lean/run/impbug4.lean
@@ -1,18 +1,18 @@
 -- category
 
 definition Prop := Type.{0}
-variable eq {A : Type} : A → A → Prop
+constant eq {A : Type} : A → A → Prop
 infix `=`:50 := eq
 
-variable ob  : Type.{1}
-variable mor : ob → ob → Type.{1}
+constant ob  : Type.{1}
+constant mor : ob → ob → Type.{1}
 
 inductive category : Type :=
 mk : Π (id : Π (A : ob), mor A A),
      (Π (A B : ob) (f : mor A A), id A = f) → category
 
 definition id (Cat : category) := category.rec (λ id idl, id) Cat
-variable Cat : category
+constant Cat : category
 
 set_option unifier.computation true
 print "-----------------"
diff --git a/tests/lean/run/implicit.lean b/tests/lean/run/implicit.lean
index f9d0c10a5..82b522bc7 100644
--- a/tests/lean/run/implicit.lean
+++ b/tests/lean/run/implicit.lean
@@ -3,7 +3,7 @@ import logic
 definition f {A : Type} {B : Type} (f : A → B → Prop) ⦃C : Type⦄ {R : C → C → Prop} {c : C} (H : R c c) : R c c
 := H
 
-variable g : Prop → Prop → Prop
-variable H : true ∧ true
+constant g : Prop → Prop → Prop
+constant H : true ∧ true
 
 check f g H
diff --git a/tests/lean/run/ind_bug.lean b/tests/lean/run/ind_bug.lean
index 540669716..65c42fc7f 100644
--- a/tests/lean/run/ind_bug.lean
+++ b/tests/lean/run/ind_bug.lean
@@ -1,6 +1,6 @@
 import logic
-variable N : Type.{1}
-variable I : Type.{1}
+constant N : Type.{1}
+constant I : Type.{1}
 
 namespace foo
   inductive p (a : N) : Prop :=
diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean
index 44fdac565..d1914894b 100644
--- a/tests/lean/run/induniv.lean
+++ b/tests/lean/run/induniv.lean
@@ -9,7 +9,7 @@ section
   cons2   : A → list2 → list2
 end
 
-variable num : Type.{1}
+constant num : Type.{1}
 
 namespace Tree
 inductive tree (A : Type) : Type :=
diff --git a/tests/lean/run/local_using.lean b/tests/lean/run/local_using.lean
index a9412c70d..b84221bcc 100644
--- a/tests/lean/run/local_using.lean
+++ b/tests/lean/run/local_using.lean
@@ -1,19 +1,19 @@
-variable N : Type.{1}
+constant N : Type.{1}
 precedence `+`:65
 
 namespace foo
-  variable a : N
-  variable f : N → N → N
+  constant a : N
+  constant f : N → N → N
   infix + := f
 end foo
 
 namespace bla
-  variable b : N
-  variable f : N → N → N
+  constant b : N
+  constant f : N → N → N
   infix + := f
 end bla
 
-variable g : N → N → N
+constant g : N → N → N
 
 open foo
 open bla
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index ff1110a11..b7905c978 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -3,7 +3,7 @@ open nat
 
 definition two1 : nat := 2
 definition two2 : nat := succ (succ (zero))
-variable f      : nat → nat → nat
+constant f      : nat → nat → nat
 
 (*
 local tc     = type_checker_with_hints(get_env(), true)
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index 2bd457fd1..8ba3f799f 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -4,8 +4,8 @@ open nat
 definition two1 : nat := 2
 definition two2 : nat := succ (succ (zero))
 definition f (x : nat) (y : nat) := y
-variable g : nat → nat → nat
-variables a b : nat
+constant g : nat → nat → nat
+constants a b : nat
 
 (*
 local tc     = type_checker_with_hints(get_env(), true)
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index 2c7bbb786..2086d80be 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -1,8 +1,8 @@
 import logic
 
-variable matrix.{l} : Type.{l} → Type.{l}
-variable same_dim {A : Type} : matrix A → matrix A → Prop
-variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
+constant matrix.{l} : Type.{l} → Type.{l}
+constant same_dim {A : Type} : matrix A → matrix A → Prop
+constant add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
 
 theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 :=
 rfl
diff --git a/tests/lean/run/matrix2.lean b/tests/lean/run/matrix2.lean
index a5c767b2d..5ec9a504e 100644
--- a/tests/lean/run/matrix2.lean
+++ b/tests/lean/run/matrix2.lean
@@ -1,8 +1,8 @@
 import logic
 
-variable matrix.{l} : Type.{l} → Type.{l}
-variable same_dim {A : Type} : matrix A → matrix A → Prop
-variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
+constant matrix.{l} : Type.{l} → Type.{l}
+constant same_dim {A : Type} : matrix A → matrix A → Prop
+constant add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
 open eq
 theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' :=
 subst H1 (subst H2 H)
diff --git a/tests/lean/run/n1.lean b/tests/lean/run/n1.lean
index 0646d8e91..7ec581b0e 100644
--- a/tests/lean/run/n1.lean
+++ b/tests/lean/run/n1.lean
@@ -1,7 +1,7 @@
-variable A : Type.{1}
-variable a : A
-variable g : A → A
-variable f : A → A → A
+constant A : Type.{1}
+constant a : A
+constant g : A → A
+constant f : A → A → A
 
 (*
 local f     = Const("f")
@@ -29,5 +29,5 @@ end
 
 notation `tst` A:(call parse_pair) := A
 notation `simple` A:(call parse_bracket) `,` B:(call parse_bracket) := f A B
-variable b : A
+constant b : A
 check g (tst (simple [b], [a]), a)
diff --git a/tests/lean/run/n2.lean b/tests/lean/run/n2.lean
index f7b9bed10..ef963e6e6 100644
--- a/tests/lean/run/n2.lean
+++ b/tests/lean/run/n2.lean
@@ -1,7 +1,7 @@
-variable A : Type.{1}
-variable a : A
-variable g : A → A
-variable f : A → A → A
+constant A : Type.{1}
+constant a : A
+constant g : A → A
+constant f : A → A → A
 precedence `|` : 0
 
 (*
diff --git a/tests/lean/run/n3.lean b/tests/lean/run/n3.lean
index e6caeb677..576d1dbd1 100644
--- a/tests/lean/run/n3.lean
+++ b/tests/lean/run/n3.lean
@@ -1,11 +1,11 @@
 definition Prop : Type.{1} := Type.{0}
-variable N : Type.{1}
-variable and : Prop → Prop → Prop
+constant N : Type.{1}
+constant and : Prop → Prop → Prop
 infixr `∧`:35 := and
-variable le : N → N → Prop
-variable lt : N → N → Prop
-variable f : N → N
-variable add : N → N → N
+constant le : N → N → Prop
+constant lt : N → N → Prop
+constant f : N → N
+constant add : N → N → N
 infixl `+`:65 := add
 precedence `≤`:50
 precedence `<`:50
@@ -14,7 +14,7 @@ infixl < := lt
 notation A ≤ B:prev ≤ C:prev := A ≤ B ∧ B ≤ C
 notation A ≤ B:prev < C:prev := A ≤ B ∧ B < C
 notation A < B:prev ≤ C:prev := A < B ∧ B ≤ C
-variables a b c d e : N
+constants a b c d e : N
 check a ≤ b ≤ f c + b ∧ a < b
 check a ≤ d
 check a < b ≤ c
diff --git a/tests/lean/run/n4.lean b/tests/lean/run/n4.lean
index c02dbf6a3..3d421f063 100644
--- a/tests/lean/run/n4.lean
+++ b/tests/lean/run/n4.lean
@@ -1,11 +1,11 @@
 definition Prop : Type.{1} := Type.{0}
 context
-  variable N : Type.{1}
-  variables a b c : N
-  variable and : Prop → Prop → Prop
+  parameter N : Type.{1}
+  parameters a b c : N
+  parameter and : Prop → Prop → Prop
   infixr `∧`:35 := and
-  variable le : N → N → Prop
-  variable lt : N → N → Prop
+  parameter le : N → N → Prop
+  parameter lt : N → N → Prop
   precedence `≤`:50
   precedence `<`:50
   infixl ≤ := le
diff --git a/tests/lean/run/n5.lean b/tests/lean/run/n5.lean
index ce8dc27bd..cc17a3bb7 100644
--- a/tests/lean/run/n5.lean
+++ b/tests/lean/run/n5.lean
@@ -1,8 +1,8 @@
-variable N : Type.{1}
-variable f : N → N → N → N
-variable g : N → N → N
-variable h : N → N → N → N
-variable s : N → N → N → N → N
+constant N : Type.{1}
+constant f : N → N → N → N
+constant g : N → N → N
+constant h : N → N → N → N
+constant s : N → N → N → N → N
 
 precedence `*`:75
 precedence `|`:75
@@ -12,7 +12,7 @@ notation a * b := g a b
 notation a * b * c:prev := h a b c
 notation a * b | c * d:prev := s a b c d
 
-variables a b c d e : N
+constants a b c d e : N
 
 check a * b
 check a * b | d
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 4aa31159d..3dbce8b55 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -12,7 +12,7 @@ definition to_nat [coercion] (n : num) : nat
 := num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
 definition add (x y : nat) : nat
 := plus x y
-variable le : nat → nat → Prop
+constant le : nat → nat → Prop
 
 infixl `+`:65 := add
 infix `≤`:50  := le
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 5c7908885..53e5c5c8f 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -12,7 +12,7 @@ definition to_nat [coercion] (n : num) : nat
 := num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n
 definition add (x y : nat) : nat
 := plus x y
-variable le : nat → nat → Prop
+constant le : nat → nat → Prop
 
 infixl `+`:65 := add
 infix `≤`:50  := le
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 90ca8ac35..eb0ddff80 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -13,7 +13,7 @@ infixl `*`:75 := mul
 
 axiom mul_zero_right (n : nat) : n * zero = zero
 
-variable P : nat → Prop
+constant P : nat → Prop
 
 print "==========================="
 theorem tst (n : nat) (H : P (n * zero)) : P zero
diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean
index c3dee868f..fbc90fb69 100644
--- a/tests/lean/run/nat_coe.lean
+++ b/tests/lean/run/nat_coe.lean
@@ -1,19 +1,19 @@
 import logic
 
-variable nat : Type.{1}
-variable int : Type.{1}
+constant nat : Type.{1}
+constant int : Type.{1}
 
-variable nat_add : nat → nat → nat
+constant nat_add : nat → nat → nat
 infixl `+`:65 := nat_add
 
-variable int_add : int → int → int
+constant int_add : int → int → int
 infixl `+`:65 := int_add
 
-variable of_nat : nat → int
+constant of_nat : nat → int
 coercion of_nat
 
-variables a b : nat
-variables i j : int
+constants a b : nat
+constants i j : int
 
 definition c1 := a + b
 
diff --git a/tests/lean/run/not_bug1.lean b/tests/lean/run/not_bug1.lean
index fdbebb13a..ae5c8f866 100644
--- a/tests/lean/run/not_bug1.lean
+++ b/tests/lean/run/not_bug1.lean
@@ -1,9 +1,9 @@
 import logic
 open bool
 
-variable list : Type.{1}
-variable nil  : list
-variable cons : bool → list → list
+constant list : Type.{1}
+constant nil  : list
+constant cons : bool → list → list
 
 infixr `::`:65 := cons
 notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
@@ -14,7 +14,7 @@ check [tt, ff]
 check [tt, ff, ff]
 check tt :: ff :: [tt, ff, ff]
 check tt :: []
-variables a b c : bool
+constants a b c : bool
 check a :: b :: nil
 check [a, b]
 check [a, b, c]
diff --git a/tests/lean/run/ns.lean b/tests/lean/run/ns.lean
index 6be6578ac..a1448a398 100644
--- a/tests/lean/run/ns.lean
+++ b/tests/lean/run/ns.lean
@@ -1,17 +1,17 @@
-variable nat : Type.{1}
-variable f : nat → nat
+constant nat : Type.{1}
+constant f : nat → nat
 
 namespace foo
-  variable int : Type.{1}
-  variable f   : int → int
-  variable a   : nat
-  variable i   : int
+  constant int : Type.{1}
+  constant f   : int → int
+  constant a   : nat
+  constant i   : int
   check _root_.f a
   check f i
 end foo
 
 open foo
-variables a : nat
-variables i : int
+constants a : nat
+constants i : int
 check f a
 check f i
diff --git a/tests/lean/run/ns2.lean b/tests/lean/run/ns2.lean
index d080c2021..321b37954 100644
--- a/tests/lean/run/ns2.lean
+++ b/tests/lean/run/ns2.lean
@@ -1,5 +1,5 @@
 definition foo.id {A : Type} (a : A) := a
-variable foo.T : Type.{1}
+constant foo.T : Type.{1}
 check foo.id
 check foo.T
 
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index e40662a25..47a50b1d8 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/tests/lean/run/occurs_check_bug1.lean
@@ -3,10 +3,10 @@ import logic data.nat data.prod
 open nat prod
 open decidable
 
-variable modulo (x : ℕ) (y : ℕ) : ℕ
+constant modulo (x : ℕ) (y : ℕ) : ℕ
 infixl `mod`:70 := modulo
 
-variable gcd_aux : ℕ × ℕ → ℕ
+constant gcd_aux : ℕ × ℕ → ℕ
 
 definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)
 
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
index 70ef84fb4..938d6aed4 100644
--- a/tests/lean/run/opaque_hint_bug.lean
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -4,7 +4,7 @@ cons : T → list T → list T
 
 
 section
-  variable {T : Type}
+  parameter {T : Type}
 
   definition concat (s t : list T) : list T
   := list.rec t (fun x l u, list.cons x u) s
diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
index c6cbd9e88..93c9e9d3d 100644
--- a/tests/lean/run/over_subst.lean
+++ b/tests/lean/run/over_subst.lean
@@ -1,10 +1,10 @@
 import logic
 
 namespace nat
-variable nat : Type.{1}
-variable add : nat → nat → nat
-variable le : nat → nat → Prop
-variable one : nat
+constant nat : Type.{1}
+constant add : nat → nat → nat
+constant le : nat → nat → Prop
+constant one : nat
 infixl `+`:65 := add
 infix `≤`:50 := le
 axiom add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
@@ -12,10 +12,10 @@ axiom add_le_left {a b : nat} (H : a ≤ b) (c : nat) : c + a ≤ c + b
 end nat
 
 namespace int
-variable int : Type.{1}
-variable add : int → int → int
-variable le : int → int → Prop
-variable one : int
+constant int : Type.{1}
+constant add : int → int → int
+constant le : int → int → Prop
+constant one : int
 infixl `+`:65 := add
 infix `≤`:50  := le
 axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c)
diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean
index 61bf52ae5..a443a627d 100644
--- a/tests/lean/run/root.lean
+++ b/tests/lean/run/root.lean
@@ -1,14 +1,14 @@
 import logic
 
 
-variable foo : Prop
+constant foo : Prop
 
 namespace N1
-  variable foo : Prop
+  constant foo : Prop
   check N1.foo
   check _root_.foo
   namespace N2
-    variable foo : Prop
+    constant foo : Prop
     check N1.foo
     check N1.N2.foo
     print raw foo
diff --git a/tests/lean/run/secnot.lean b/tests/lean/run/secnot.lean
index e5ee67637..96e1391d9 100644
--- a/tests/lean/run/secnot.lean
+++ b/tests/lean/run/secnot.lean
@@ -14,7 +14,7 @@ cons   : T → list T → list T
 
 namespace list
 section
-variable {T : Type}
+parameter {T : Type}
 notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check [10, 20, 30]
 end
diff --git a/tests/lean/run/section2.lean b/tests/lean/run/section2.lean
index 3a637d538..3ae84ed44 100644
--- a/tests/lean/run/section2.lean
+++ b/tests/lean/run/section2.lean
@@ -3,7 +3,7 @@ import data.nat
 section foo
   parameter A : Type
   definition id (a : A) := a
-  variable a : nat
+  parameter a : nat
   check _root_.id nat a
 end foo
 
@@ -11,7 +11,7 @@ namespace n1
 section foo
   parameter A : Type
   definition id (a : A) := a
-  variable a : nat
+  parameter a : nat
   check n1.id _ a
 end foo
 end n1
diff --git a/tests/lean/run/t11.lean b/tests/lean/run/t11.lean
index bd5350f8a..cd0596e5e 100644
--- a/tests/lean/run/t11.lean
+++ b/tests/lean/run/t11.lean
@@ -1,6 +1,6 @@
-parameter A : Type.{1}
-parameters a b c : A
-parameter f : A → A → A
+constant A : Type.{1}
+constants a b c : A
+constant f : A → A → A
 check f a b
 section
   parameters A B : Type
@@ -11,4 +11,4 @@ section
   definition g (a : A) (b : B) (c : C) : A := e
 end
 check g.{2 1}
-variables x y : A
+constants x y : A
diff --git a/tests/lean/run/t3.lean b/tests/lean/run/t3.lean
index 4cbddd8f4..ff469a268 100644
--- a/tests/lean/run/t3.lean
+++ b/tests/lean/run/t3.lean
@@ -1,22 +1,22 @@
-variable int : Type.{1}
-variable nat : Type.{1}
+constant int : Type.{1}
+constant nat : Type.{1}
 namespace int
-variable plus : int → int → int
+constant plus : int → int → int
 end int
 
 namespace nat
-variable plus : nat → nat → nat
+constant plus : nat → nat → nat
 end nat
 
 open int nat
 
-variables a b : int
+constants a b : int
 
 
 check plus a b
 
-variable f : int → int → int
-variable g : nat → nat → int
+constant f : int → int → int
+constant g : nat → nat → int
 notation A `+`:65 B:65 := f A (g B B)
-variable n : nat
+constant n : nat
 check a + n
diff --git a/tests/lean/run/t4.lean b/tests/lean/run/t4.lean
index d3061d4c0..93da56767 100644
--- a/tests/lean/run/t4.lean
+++ b/tests/lean/run/t4.lean
@@ -3,7 +3,7 @@ namespace foo
   check f.{1}
 end foo
 
-variable N : Type.{1}
+constant N : Type.{1}
 section
   parameter A : Type
   definition g (a : A) (B : Type) : A := a
diff --git a/tests/lean/run/t5.lean b/tests/lean/run/t5.lean
index 8d9e2eec4..4f7e78d4b 100644
--- a/tests/lean/run/t5.lean
+++ b/tests/lean/run/t5.lean
@@ -1,8 +1,8 @@
-variable N : Type.{1}
+constant N : Type.{1}
 namespace foo
-  variable N : Type.{2}
+  constant N : Type.{2}
   namespace tst
-    variable N : Type.{3}
+    constant N : Type.{3}
     print raw N
   end tst
 end foo
@@ -12,8 +12,8 @@ namespace foo
   namespace tst
     print raw N N -> N
     section
-      variable N : Type.{4} -- Shadow previous ones.
+      parameter N : Type.{4} -- Shadow previous ones.
       print raw N
     end
   end tst
-end  foo
\ No newline at end of file
+end  foo
diff --git a/tests/lean/run/t6.lean b/tests/lean/run/t6.lean
index 706080e09..e8e3bff00 100644
--- a/tests/lean/run/t6.lean
+++ b/tests/lean/run/t6.lean
@@ -1,8 +1,8 @@
 precedence `+`  : 65
 precedence `++` : 100
-variable N : Type.{1}
-variable f : N → N → N
-variable a : N
+constant N : Type.{1}
+constant f : N → N → N
+constant a : N
 check
    let g x y         := f x y,
        infix +       := g,
diff --git a/tests/lean/run/t7.lean b/tests/lean/run/t7.lean
index 7f1684146..8ed803eed 100644
--- a/tests/lean/run/t7.lean
+++ b/tests/lean/run/t7.lean
@@ -1,3 +1,3 @@
-variable A : Type.{1}
-variable f : A → A → A
-print raw f _ (f _ _)
\ No newline at end of file
+constant A : Type.{1}
+constant f : A → A → A
+print raw f _ (f _ _)
diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean
index 877ee06e5..42f5e2cda 100644
--- a/tests/lean/run/tactic15.lean
+++ b/tests/lean/run/tactic15.lean
@@ -1,8 +1,8 @@
 import logic
 open tactic
 
-variable A : Type.{1}
-variable f : A → A → A
+constant A : Type.{1}
+constant f : A → A → A
 open eq
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c)
 := by apply (subst H1);
diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean
index 3797719db..aa7102f37 100644
--- a/tests/lean/run/tactic16.lean
+++ b/tests/lean/run/tactic16.lean
@@ -1,8 +1,8 @@
 import logic data.string
 open tactic
 
-variable A : Type.{1}
-variable f : A → A → A
+constant A : Type.{1}
+constant f : A → A → A
 open eq
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c)
 := by discard (apply (subst H1)) 3;  -- discard the first 3 solutions produced by apply
diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean
index 19b04185a..f4c89853d 100644
--- a/tests/lean/run/tactic17.lean
+++ b/tests/lean/run/tactic17.lean
@@ -1,8 +1,8 @@
 import logic
 open tactic
 
-variable A : Type.{1}
-variable f : A → A → A
+constant A : Type.{1}
+constant f : A → A → A
 
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
 := by apply (@congr A A (f a) (f b));
diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean
index 12fbe08cf..3ea937658 100644
--- a/tests/lean/run/tactic18.lean
+++ b/tests/lean/run/tactic18.lean
@@ -1,8 +1,8 @@
 import logic
 open tactic
 
-variable A : Type.{1}
-variable f : A → A → A
+constant A : Type.{1}
+constant f : A → A → A
 
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
 := by apply (@congr A A);
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index f9527f4f9..acb773229 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -4,7 +4,7 @@ inductive nat : Type :=
 zero : nat,
 succ : nat → nat
 
-variable f : nat → nat
+constant f : nat → nat
 
 check @nat.rec
 
diff --git a/tests/lean/run/unicode.lean b/tests/lean/run/unicode.lean
index 9a8bc28e8..082f98859 100644
--- a/tests/lean/run/unicode.lean
+++ b/tests/lean/run/unicode.lean
@@ -1,10 +1,10 @@
 import logic
 
-variable N : Type
-variable α : N
-variable β₁ : N
+constant N : Type
+constant α : N
+constant β₁ : N
 check β₁
-variable δ : N
+constant δ : N
 check δ
-variable δ₁₁ : N
+constant δ₁₁ : N
 check δ₁₁
diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
index 382d17f05..ce3b41646 100644
--- a/tests/lean/run/univ1.lean
+++ b/tests/lean/run/univ1.lean
@@ -1,20 +1,20 @@
 import logic
 
 namespace S1
-hypothesis I : Type
+axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
-hypothesis unfold.{l} : I.{l} → F I.{l}
-hypothesis fold.{l}   : F I.{l} → I.{l}
-hypothesis iso1 : ∀x, fold (unfold x) = x
+axiom unfold.{l} : I.{l} → F I.{l}
+axiom fold.{l}   : F I.{l} → I.{l}
+axiom iso1 : ∀x, fold (unfold x) = x
 end S1
 
 namespace S2
 universe u
-hypothesis I : Type.{u}
+axiom I : Type.{u}
 definition F (X : Type) : Type := (X → Prop) → Prop
-hypothesis unfold : I → F I
-hypothesis fold   : F I → I
-hypothesis iso1 : ∀x, fold (unfold x) = x
+axiom unfold : I → F I
+axiom fold   : F I → I
+axiom iso1 : ∀x, fold (unfold x) = x
 end S2
 
 
diff --git a/tests/lean/run/univ2.lean b/tests/lean/run/univ2.lean
index fd281567e..6172119a3 100644
--- a/tests/lean/run/univ2.lean
+++ b/tests/lean/run/univ2.lean
@@ -1,10 +1,10 @@
 import logic
 
-hypothesis I : Type
+axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
-hypothesis unfold : I → F I
-hypothesis fold   : F I → I
-hypothesis iso1 : ∀x, fold (unfold x) = x
+axiom unfold : I → F I
+axiom fold   : F I → I
+axiom iso1 : ∀x, fold (unfold x) = x
 
 theorem iso2 : ∀x, fold (unfold x) = x
 := sorry
diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean
index 6e56b9474..4efbb3d37 100644
--- a/tests/lean/show1.lean
+++ b/tests/lean/show1.lean
@@ -1,7 +1,7 @@
 import logic
 open bool eq.ops tactic
 
-variables a b c : bool
+constants a b c : bool
 axiom H1 : a = b
 axiom H2 : b = c
 
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 905d1c675..8bdbce5c5 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -31,7 +31,7 @@ infix `::` : 65 := cons
 
 section
 
-variable {T : Type}
+parameter {T : Type}
 
 theorem list_induction_on {P : list T → Prop} (l : list T) (Hnil : P nil)
     (Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l :=
diff --git a/tests/lean/t10.lean b/tests/lean/t10.lean
index 6e111f902..b19cc36bf 100644
--- a/tests/lean/t10.lean
+++ b/tests/lean/t10.lean
@@ -1,20 +1,20 @@
-variable N : Type.{1}
+constant N : Type.{1}
 definition B : Type.{1} := Type.{0}
-variable ite : B → N → N → N
-variable and : B → B → B
-variable f : N → N
-variable p : B
-variable q : B
-variable x : N
-variable y : N
-variable z : N
+constant ite : B → N → N → N
+constant and : B → B → B
+constant f : N → N
+constant p : B
+constant q : B
+constant x : N
+constant y : N
+constant z : N
 infixr `∧`:25 := and
 notation `if` c `then` t `else` e := ite c t e
 check if p ∧ q then f x else y
 check if p ∧ q then q else y
-variable list : Type.{1}
-variable nil : list
-variable cons : N → list → list
+constant list : Type.{1}
+constant nil : list
+constant cons : N → list → list
 -- Non empty lists
 notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check [x, y, z, x, y, y]
diff --git a/tests/lean/t11.lean b/tests/lean/t11.lean
index 88f7bb731..a5af8c297 100644
--- a/tests/lean/t11.lean
+++ b/tests/lean/t11.lean
@@ -1,10 +1,10 @@
-variable A    : Type.{1}
+constant A    : Type.{1}
 definition bool : Type.{1} := Type.{0}
-variable Exists (P : A → bool) : bool
+constant Exists (P : A → bool) : bool
 notation `exists` binders `,` b:(scoped b, Exists b) := b
 notation `∃` binders `,` b:(scoped b, Exists b) := b
-variable p : A → bool
-variable q : A → A → bool
+constant p : A → bool
+constant q : A → A → bool
 check exists x : A, p x
 check ∃ x y : A, q x y
 notation `{` binder `|` b:scoped `}` := b
diff --git a/tests/lean/t12.lean b/tests/lean/t12.lean
index 392df1b06..9b9f2afcf 100644
--- a/tests/lean/t12.lean
+++ b/tests/lean/t12.lean
@@ -1,7 +1,7 @@
 precedence `+` : 65
 precedence `*` : 75
-variable N : Type.{1}
+constant N : Type.{1}
 check λ (f : N -> N -> N) (g : N → N → N) (infix + := f) (infix * := g) (x y : N), x+x*y
-variable f : N → N → N
-variable a : N
+constant f : N → N → N
+constant a : N
 check a+a -- + notation is not available anymore
diff --git a/tests/lean/t13.lean b/tests/lean/t13.lean
index a4bbef515..cdf9bdb24 100644
--- a/tests/lean/t13.lean
+++ b/tests/lean/t13.lean
@@ -1,12 +1,12 @@
-variable A : Type.{1}
-variable f : A → A → A
-variable g : A → A → A
+constant A : Type.{1}
+constant f : A → A → A
+constant g : A → A → A
 precedence `+` : 65
 infixl + := f
 infixl + := g
-variable a : A
-variable b : A
+constant a : A
+constant b : A
 print raw a+b -- + is overloaded
 check fun (h : A → A → A)
           (infixl + := h), -- Like local declarations, local notation "shadows" global one.
-      a+b
\ No newline at end of file
+      a+b
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index a21361231..7850c5a2d 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -1,8 +1,8 @@
 namespace foo
-  variable A : Type.{1}
-  variable a : A
-  variable x : A
-  variable c : A
+  constant A : Type.{1}
+  constant a : A
+  constant x : A
+  constant c : A
 end foo
 
 context
@@ -31,7 +31,7 @@ context
 end
 
 namespace foo
-  variable f : A → A → A
+  constant f : A → A → A
   infix `*`:75 := f
 end foo
 
diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean
index 070048d4b..d2812d831 100644
--- a/tests/lean/t4.lean
+++ b/tests/lean/t4.lean
@@ -1,21 +1,21 @@
 definition Prop : Type.{1} := Type.{0}
-variable N : Type.{1}
+constant N : Type.{1}
 check N
-variable a : N
+constant a : N
 check a
 check Prop → Prop
-variable F.{l} : Type.{l} → Type.{l}
+constant F.{l} : Type.{l} → Type.{l}
 check F.{2}
 universe u
 check F.{u}
-variable vec.{l} (A : Type.{l}) (n : N) : Type.{l}
-variable f (a b : N) : N
-variable len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
+constant vec.{l} (A : Type.{l}) (n : N) : Type.{l}
+constant f (a b : N) : N
+constant len.{l} (A : Type.{l}) (n : N) (v : vec.{l} A n) : N
 check f
 check len.{1}
 section
-   variable A  : Type
-   variable B  : Prop
+   parameter A  : Type
+   parameter B  : Prop
    hypothesis H : B
    parameter {C : Type}
    check B -> B
@@ -24,20 +24,20 @@ section
 end
 check A -- Error: A is part of the section
 
-variable R : Type → Type
+constant R : Type → Type
 check R.{1 0}
 
 check fun x y : N, x
 
 namespace tst
-  variable N : Type.{2}
-  variable M : Type.{2}
+  constant N : Type.{2}
+  constant M : Type.{2}
   print raw N -- Two possible interpretations N and tst.N
   print raw tst.N -- Only one interpretation
 end tst
 print raw N -- Only one interpretation
 namespace foo
-  variable M : Type.{3}
+  constant M : Type.{3}
   print raw M -- Only one interpretation
 end foo
 check tst.M
@@ -56,4 +56,4 @@ print("-------------")
 *)
 
 universe l_1
-variable T1 : Type -- T1 parameter is going to be called l_2
+constant T1 : Type -- T1 parameter is going to be called l_2
diff --git a/tests/lean/t5.lean b/tests/lean/t5.lean
index fcaf337c2..f53b33026 100644
--- a/tests/lean/t5.lean
+++ b/tests/lean/t5.lean
@@ -1,6 +1,6 @@
-variable N : Type.{1}
-variable f : N → N
-variable a : N
+constant N : Type.{1}
+constant f : N → N
+constant a : N
 definition g (a : N) : N := f a
 check g
 namespace foo
diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean
index 4de279db5..f552bcb7b 100644
--- a/tests/lean/t7.lean
+++ b/tests/lean/t7.lean
@@ -1,5 +1,5 @@
 definition Prop : Type.{1} := Type.{0}
-variable and : Prop → Prop → Prop
+constant and : Prop → Prop → Prop
 section
   parameter {A : Type}  -- Mark A as implicit parameter
   parameter   R : A → A → Prop
diff --git a/tests/lean/t9.lean b/tests/lean/t9.lean
index 804b776cd..4c0afbe75 100644
--- a/tests/lean/t9.lean
+++ b/tests/lean/t9.lean
@@ -2,11 +2,11 @@ precedence `+` : 65
 precedence `*` : 75
 precedence `=` : 50
 precedence `≃` : 50
-variable N : Type.{1}
-variable a : N
-variable b : N
-variable add : N → N → N
-variable mul : N → N → N
+constant N : Type.{1}
+constant a : N
+constant b : N
+constant add : N → N → N
+constant mul : N → N → N
 namespace foo
   infixl + := add
   infixl * := mul
diff --git a/tests/lean/uni_bug1.lean b/tests/lean/uni_bug1.lean
index 098c846cd..11151b014 100644
--- a/tests/lean/uni_bug1.lean
+++ b/tests/lean/uni_bug1.lean
@@ -1,8 +1,8 @@
 import data.nat.basic data.prod
 open nat prod
 
-variable R : nat → nat → Prop
-variable f (a b : nat) (H : R a b) : nat
+constant R : nat → nat → Prop
+constant f (a b : nat) (H : R a b) : nat
 axiom Rtrue (a b : nat) : R a b