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

@@ -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.

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
+  constant n : nat
-  variable m : nat
+  constant m : nat
-  variable o : 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

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 :=

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 :=

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))))

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));
 }
 }

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"},
+        {{"lemma", "theorem"}, {"corollary", "theorem"}, {"hypothesis", "parameter"}, {"conjecture", "parameter"},
-         {"hypothesis", "axiom"}, {"conjecture", "axiom"}, {"corollary", "theorem"},
          {nullptr, nullptr}};
 
     auto it = builtin;

tests/lean/alias.lean

@@ -1,18 +1,18 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
+  constant num : Type.{1}
-  variable foo : num → num → num
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
+  constant val : Type.{1}
-  variable foo : val → val → val
+  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

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

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

tests/lean/choice_expl.lean

@@ -7,8 +7,8 @@ namespace N2
 end N2
 
 open N1 N2
-variable N : Type.{1}
+constant N : Type.{1}
-variables a b : N
+constants a b : N
 check @pr
 check @pr N a b
 check pr a 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

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
 

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)
 

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
+constant n : nat
-variable i : int
+constant i : int
 check n + i

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

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,

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}
+constant N : Type.{1}
-variable z : N
+constant z : N
-variable o : N
+constant o : N
-variable b : 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}
+constant G : Type.{1}
-variable gz : G
+constant gz : G
-variable a  : G
+constant a  : G
 
 notation 0 := gz
 

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}
+constant N : Type.{1}
-variable z : N
+constant z : N
-variable o : N
+constant o : N
-variable a : N
+constant a : N
 
 notation 0 := z
 notation 1 := o

tests/lean/num4.lean

@@ -3,10 +3,10 @@ set_option pp.notation false
 set_option pp.implicit true
 
 namespace foo
-  variable N : Type.{1}
+  constant N : Type.{1}
-  variable z : N
+  constant z : N
-  variable o : N
+  constant o : N
-  variable a : N
+  constant a : N
   notation 0 := z
   notation 1 := o
 

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|

tests/lean/run/algebra1.lean

@@ -38,8 +38,8 @@ end algebra
 
 namespace nat
 
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
-  variable mul : 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
+  parameter M : monoid
-  variables a b c : M
+  parameters a b c : M
   check a*b*c*a*b*c*a*b*a*b*c*a
   check a*b
 end

tests/lean/run/alias1.lean

@@ -1,25 +1,25 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
+  constant num : Type.{1}
-  variable foo : num → num → num
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
+  constant val : Type.{1}
-  variable foo : val → val → val
+  constant foo : val → val → val
 end N2
 
 open N1
 open N2
-variables a b : num
+constants a b : num
-variables x y : val
+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

tests/lean/run/alias2.lean

@@ -1,19 +1,19 @@
 import logic
 
 namespace N1
-  variable num : Type.{1}
+  constant num : Type.{1}
-  variable foo : num → num → num
+  constant foo : num → num → num
 end N1
 
 namespace N2
-  variable val : Type.{1}
+  constant val : Type.{1}
-  variable foo : val → val → val
+  constant foo : val → val → val
 end N2
 
 open N1
 open N2
-variables a b : num
+constants a b : num
-variable f : num → val
+constant f : num → val
 coercion f
 
 definition aux2 := foo a 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

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}
+constant group.{l} : Type.{l+1}
-variable carrier.{l} : group.{l} → Type.{l}
+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}

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
+  parameters x y : A
-  axiom H : x = y
+  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
+  parameters x y : A
-  axiom H : x = y
+  hypothesis H : x = y
   check T2 H
   check T2
 end

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

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

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

tests/lean/run/class5.lean

@@ -15,8 +15,8 @@ namespace nat
   zero : nat,
   succ : nat → nat
 
-  variable mul : nat → nat → nat
+  constant mul : nat → nat → nat
-  variable add : 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

tests/lean/run/class_coe.lean

@@ -1,10 +1,10 @@
 import data.num
 
 
-variables int nat real : Type.{1}
+constants int nat real : Type.{1}
-variable nat_add  : nat → nat → nat
+constant nat_add  : nat → nat → nat
-variable int_add  : int → int → int
+constant int_add  : int → int → int
-variable real_add : real → real → real
+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
+constants n m : nat
-variables i j : int
+constants i j : int
-variables x y : real
+constants x y : real
-variable num_to_nat : num → nat
+constant num_to_nat : num → nat
-variable nat_to_int : nat → int
+constant nat_to_int : nat → int
-variable int_to_real : int → real
+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

tests/lean/run/coe1.lean

@@ -1,15 +1,15 @@
-variable A : Type.{1}
+constant A : Type.{1}
-variable B : Type.{1}
+constant B : Type.{1}
-variable f : A → B
+constant f : A → B
 coercion f
-variable g : B → B → B
+constant g : B → B → B
-variables a1 a2 a3 : A
+constants a1 a2 a3 : A
-variables b1 b2 b3 : B
+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

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
+constant f : fn2 Prop nat nat
-variable a : Prop
+constant a : Prop
-variable n : nat
+constant n : nat
 check f a
 check f n

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
+constants obC obD : Type
-variables a b : obC
+constants a b : obC
-variable C : category obC
+constant C : category obC
 instance C
-variable D : category obD
+constant D : category obD
-variable F : my_functor C D
+constant F : my_functor C D
-variable m : mor a b
+constant m : mor a b
 check F a
 check F m

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
+constant f : foo nat nat
-variable a : nat
+constant a : nat
 check f a true

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
+constant S : struct
-variable a : S
+constant a : S
 
 check id (struct.to_sort S) a
 check id S a

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
+constant S : struct
-variable a : S
+constant a : S
 
 check id (struct.to_sort S) a
 check id S a

tests/lean/run/coe6.lean

@@ -1,12 +1,12 @@
 import data.unit
 open unit
 
-variable int : Type.{1}
+constant int : Type.{1}
-variable nat : Type.{1}
+constant nat : Type.{1}
-variable izero : int
+constant izero : int
-variable nzero : nat
+constant nzero : nat
-variable isucc : int → int
+constant isucc : int → int
-variable nsucc : nat → nat
+constant nsucc : nat → nat
 definition f [coercion] (a : unit) : int := izero
 definition g [coercion] (a : unit) : nat := nzero
 

tests/lean/run/coe7.lean

@@ -1,8 +1,8 @@
 import logic
 
-variable nat : Type.{1}
+constant nat : Type.{1}
-variable int : Type.{1}
+constant int : Type.{1}
-variable of_nat : nat → int
+constant of_nat : nat → int
 coercion of_nat
 
 theorem tst (n : nat) : n = n :=

tests/lean/run/coe8.lean

@@ -1,16 +1,16 @@
 import logic
 
-variable nat : Type.{1}
+constant nat : Type.{1}
-variable int : Type.{1}
+constant int : Type.{1}
-variable of_nat : nat → int
+constant of_nat : nat → int
 coercion of_nat
-variable nat_add : nat → nat → nat
+constant nat_add : nat → nat → nat
-variable int_add : int → int → int
+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

tests/lean/run/coe9.lean

@@ -1,25 +1,25 @@
 import data.nat
 open nat
 
-variable list.{l} : Type.{l} → Type.{l}
+constant list.{l} : Type.{l} → Type.{l}
-variable vector.{l} : Type.{l} → nat → Type.{l}
+constant vector.{l} : Type.{l} → nat → Type.{l}
-variable matrix.{l} : Type.{l} → nat → nat → Type.{l}
+constant matrix.{l} : Type.{l} → nat → nat → Type.{l}
-variable length : Pi {A : Type}, list A → nat
+constant length : Pi {A : Type}, list A → nat
 
-variable list_to_vec {A : Type} (l : list A) : vector A (length l)
+constant 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
+constant 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
+constant 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 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
+constant f {A : Type} {n : nat} (M : matrix A n 1) : nat
-variable g {A : Type} {n : nat} (M : matrix A 1 n) : nat
+constant g {A : Type} {n : nat} (M : matrix A 1 n) : nat
-variable v : vector nat 10
+constant v : vector nat 10
-variable l : list nat
+constant l : list nat
 
 check f v
 check g v

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}
+constant n : Type.{1}
-variable f : fn n n
+constant f : fn n n
-variable a : obj n
+constant a : obj n
 check (f a)

tests/lean/run/ctx.lean

@@ -1,8 +1,8 @@
 import data.nat logic.core.inhabited
 open nat inhabited
 
-variable N : Type.{1}
+constant N : Type.{1}
-variable a : N
+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

tests/lean/run/decidable.lean

@@ -1,7 +1,7 @@
 import logic data.unit
 open bool unit decidable
 
-variables a b c : bool
+constants a b c : bool
-variables u v : unit
+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

tests/lean/run/e1.lean

@@ -1,15 +1,15 @@
 definition Prop : Type.{1} := Type.{0}
-variable eq : forall {A : Type}, A → A → Prop
+constant eq : forall {A : Type}, A → A → Prop
-variable N : Type.{1}
+constant N : Type.{1}
-variables a b c : N
+constants a b c : N
 infix `=`:50 := eq
 check a = b
 
-variable f : Prop → N → N
+constant f : Prop → N → N
-variable g : N → 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

tests/lean/run/e10.lean

@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+  parameters n m : nat
-  variables i j : int
+  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

tests/lean/run/e11.lean

@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+  parameters n m : nat
-  variables i j : int
+  parameters i j : int
   check n + m
   check i + j
 

tests/lean/run/e12.lean

@@ -1,22 +1,22 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+constants n m : nat.nat
-variables i j : int.int
+constants i j : int.int
 
 section
   open [notation] nat

tests/lean/run/e13.lean

@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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

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)

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

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

tests/lean/run/e17.lean

@@ -12,8 +12,8 @@ neg : nat → int
 
 coercion int.of_nat
 
-variables n m : nat
+constants n m : nat
-variables i j : int
+constants i j : int
 namespace list end list open list
 
 check cons i (cons i nil)

tests/lean/run/e18.lean

@@ -12,9 +12,9 @@ neg : nat → int
 
 coercion int.of_nat
 
-variables n m : nat
+constants n m : nat
-variables i j : int
+constants i j : int
-variable l : list nat
+constant l : list nat
 namespace list end list open list
 
 check cons i (cons i nil)

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)

tests/lean/run/e6.lean

@@ -1,25 +1,25 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+constants n m : nat
-variables i j : int
+constants i j : int
 
 check n + m
 check i + j

tests/lean/run/e7.lean

@@ -1,25 +1,25 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+constants n m : nat
-variables i j : int
+constants i j : int
 
 -- 'Most recent' are always tried first
 print raw i + n

tests/lean/run/e8.lean

@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+constants n m : nat
-variables i j : int
+constants i j : int
 check n + m
 check i + j
 

tests/lean/run/e9.lean

@@ -1,17 +1,17 @@
 precedence `+`:65
 
 namespace nat
-  variable nat : Type.{1}
+  constant nat : Type.{1}
-  variable add : nat → nat → nat
+  constant add : nat → nat → nat
   infixl + := add
 end nat
 
 namespace int
   open nat (nat)
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable add : int → int → int
+  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
+constants n m : nat
-variables i j : int
+constants i j : int
 check n + m
 check i + j
 

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

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

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)

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

tests/lean/run/fun.lean

@@ -2,22 +2,22 @@ import logic algebra.function
 open function bool
 
 
-variable f : num → bool
+constant f : num → bool
-variable g : num → num
+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
+constant f1 : num → num → bool
-variable f2 : bool → num
+constant f2 : bool → num
 
 check (f1 on f2) ff tt

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}
+constant  G1 : group.{1}
-variable  G2 : group.{1}
+constant  G2 : group.{1}
-variables a b c : (carrier G2)
+constants a b c : (carrier G2)
-variables d e : (carrier G1)
+constants d e : (carrier G1)
 check a * b * b
 check d * e

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
+  parameter  G1 : group
-  variable  G2 : group
+  parameter  G2 : group
-  variables a b c : G2
+  parameters a b c : G2
-  variables d e   : G1
+  parameters d e   : G1
   check a * b * b
   check d * e
 end
 
-variable G : group.{1}
+constant G : group.{1}
-variables a b : G
+constants a b : G
 definition val : G := a*b
 check val
 
-variable pos_real : Type.{1}
+constant pos_real : Type.{1}
-variable rmul  : pos_real → pos_real → pos_real
+constant rmul  : pos_real → pos_real → pos_real
-variable rone  : pos_real
+constant rone  : pos_real
-variable rinv  : pos_real → 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 "---------------"

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

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

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

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

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

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
+constant and_intro : forall (a b : Prop), a → b → a ∧ b
-variables a b c d : Prop
+constants a b c d : Prop
 axiom Ha : a
 axiom Hb : b
 axiom Hc : c

tests/lean/run/imp.lean

@@ -1,6 +1,6 @@
-variable N : Type.{1}
+constant N : Type.{1}
-variables a b c : N
+constants a b c : N
-variable f : forall {a b : N}, N → 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

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 :=

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}
+constant ob  : Type.{1}
-variable mor : ob → ob → Type.{1}
+constant mor : ob → ob → Type.{1}
-variable Cat : category ob mor
+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)

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}
+constant ob  : Type.{1}
-variable mor : ob → 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)

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}
+constant ob  : Type.{1}
-variable mor : ob → 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 "-----------------"

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
+constant g : Prop → Prop → Prop
-variable H : true ∧ true
+constant H : true ∧ true
 
 check f g H

tests/lean/run/ind_bug.lean

@@ -1,6 +1,6 @@
 import logic
-variable N : Type.{1}
+constant N : Type.{1}
-variable I : Type.{1}
+constant I : Type.{1}
 
 namespace foo
   inductive p (a : N) : Prop :=

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 :=

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
+  constant a : N
-  variable f : N → N → N
+  constant f : N → N → N
   infix + := f
 end foo
 
 namespace bla
-  variable b : N
+  constant b : N
-  variable f : N → N → N
+  constant f : N → N → N
   infix + := f
 end bla
 
-variable g : N → N → N
+constant g : N → N → N
 
 open foo
 open bla

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)

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
+constant g : nat → nat → nat
-variables a b : nat
+constants a b : nat
 
 (*
 local tc     = type_checker_with_hints(get_env(), true)

tests/lean/run/matrix.lean

@@ -1,8 +1,8 @@
 import logic
 
-variable matrix.{l} : Type.{l} → Type.{l}
+constant matrix.{l} : Type.{l} → Type.{l}
-variable same_dim {A : Type} : matrix A → matrix A → Prop
+constant 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 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

tests/lean/run/matrix2.lean

@@ -1,8 +1,8 @@
 import logic
 
-variable matrix.{l} : Type.{l} → Type.{l}
+constant matrix.{l} : Type.{l} → Type.{l}
-variable same_dim {A : Type} : matrix A → matrix A → Prop
+constant 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 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)

tests/lean/run/n1.lean

@@ -1,7 +1,7 @@
-variable A : Type.{1}
+constant A : Type.{1}
-variable a : A
+constant a : A
-variable g : A → A
+constant g : A → A
-variable f : A → 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)

tests/lean/run/n2.lean

@@ -1,7 +1,7 @@
-variable A : Type.{1}
+constant A : Type.{1}
-variable a : A
+constant a : A
-variable g : A → A
+constant g : A → A
-variable f : A → A → A
+constant f : A → A → A
 precedence `|` : 0
 
 (*

tests/lean/run/n3.lean

@@ -1,11 +1,11 @@
 definition Prop : Type.{1} := Type.{0}
-variable N : Type.{1}
+constant N : Type.{1}
-variable and : Prop → Prop → Prop
+constant and : Prop → Prop → Prop
 infixr `∧`:35 := and
-variable le : N → N → Prop
+constant le : N → N → Prop
-variable lt : N → N → Prop
+constant lt : N → N → Prop
-variable f : N → N
+constant f : N → N
-variable add : N → 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

tests/lean/run/n4.lean

@@ -1,11 +1,11 @@
 definition Prop : Type.{1} := Type.{0}
 context
-  variable N : Type.{1}
+  parameter N : Type.{1}
-  variables a b c : N
+  parameters a b c : N
-  variable and : Prop → Prop → Prop
+  parameter and : Prop → Prop → Prop
   infixr `∧`:35 := and
-  variable le : N → N → Prop
+  parameter le : N → N → Prop
-  variable lt : N → N → Prop
+  parameter lt : N → N → Prop
   precedence `≤`:50
   precedence `<`:50
   infixl ≤ := le

tests/lean/run/n5.lean

@@ -1,8 +1,8 @@
-variable N : Type.{1}
+constant N : Type.{1}
-variable f : N → N → N → N
+constant f : N → N → N → N
-variable g : N → N → N
+constant g : N → N → N
-variable h : N → N → N → N
+constant h : N → N → N → N
-variable s : N → 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

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

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

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

tests/lean/run/nat_coe.lean

@@ -1,19 +1,19 @@
 import logic
 
-variable nat : Type.{1}
+constant nat : Type.{1}
-variable int : 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
+constants a b : nat
-variables i j : int
+constants i j : int
 
 definition c1 := a + b
 

tests/lean/run/not_bug1.lean

@@ -1,9 +1,9 @@
 import logic
 open bool
 
-variable list : Type.{1}
+constant list : Type.{1}
-variable nil  : list
+constant nil  : list
-variable cons : bool → list → 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]

tests/lean/run/ns.lean

@@ -1,17 +1,17 @@
-variable nat : Type.{1}
+constant nat : Type.{1}
-variable f : nat → nat
+constant f : nat → nat
 
 namespace foo
-  variable int : Type.{1}
+  constant int : Type.{1}
-  variable f   : int → int
+  constant f   : int → int
-  variable a   : nat
+  constant a   : nat
-  variable i   : int
+  constant i   : int
   check _root_.f a
   check f i
 end foo
 
 open foo
-variables a : nat
+constants a : nat
-variables i : int
+constants i : int
 check f a
 check f i

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
 

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)
 

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