From 68110faa4d414023418ba1e79c514215440b6066 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Feb 2015 17:00:10 -0800
Subject: [PATCH] feat(frontends/lean/inductive_cmd): allow '|' in inductive
 datatype declarations

---
 hott/init/datatypes.hlean               | 30 +++++++++++-----------
 hott/init/logic.hlean                   |  4 +--
 hott/init/nat.hlean                     |  4 +--
 hott/init/relation.hlean                |  4 +--
 hott/init/tactic.hlean                  |  4 +--
 hott/init/trunc.hlean                   |  4 +--
 hott/init/types/prod.hlean              |  4 +--
 library/data/fin.lean                   |  4 +--
 library/data/int/basic.lean             |  4 +--
 library/data/list/basic.lean            |  4 +--
 library/data/vector.lean                |  4 +--
 library/init/datatypes.lean             | 34 ++++++++++++-------------
 library/init/logic.lean                 |  4 +--
 library/init/nat.lean                   |  4 +--
 library/init/prod.lean                  |  4 +--
 library/init/relation.lean              |  4 +--
 library/init/sigma.lean                 |  4 +--
 library/init/tactic.lean                |  4 +--
 src/frontends/lean/inductive_cmd.cpp    |  8 +++++-
 tests/lean/K_bug.lean                   |  2 +-
 tests/lean/bad_eqns.lean                |  8 +++---
 tests/lean/error_full_names.lean        |  2 +-
 tests/lean/ftree.lean                   | 12 ++++-----
 tests/lean/hott/cases.hlean             |  4 +--
 tests/lean/hott/eq1.hlean               |  4 +--
 tests/lean/hott/inv_bug.hlean           |  6 ++---
 tests/lean/hott/noc_list.hlean          |  4 +--
 tests/lean/hott/tele.hlean              |  4 +--
 tests/lean/interactive/auto_comp.input  |  4 +--
 tests/lean/interactive/extra_type.input |  4 +--
 tests/lean/interactive/missing.lean     |  2 +-
 tests/lean/interactive/num2.lean        |  4 +--
 tests/lean/inv_del.lean                 |  4 +--
 tests/lean/no_confusion_type.lean       |  2 +-
 tests/lean/notation2.lean               |  2 +-
 tests/lean/notation3.lean               |  2 +-
 tests/lean/notation4.lean               |  2 +-
 tests/lean/proj.lean                    |  4 +--
 tests/lean/run/331.lean                 |  4 +--
 tests/lean/run/algebra1.lean            |  4 +--
 tests/lean/run/alias3.lean              |  4 +--
 tests/lean/run/cast_sorry_bug.lean      |  4 +--
 tests/lean/run/class4.lean              |  4 +--
 tests/lean/run/class5.lean              |  4 +--
 tests/lean/run/coercion_bug2.lean       |  4 +--
 tests/lean/run/confuse_ind.lean         |  6 ++---
 tests/lean/run/e14.lean                 | 12 ++++-----
 tests/lean/run/e15.lean                 | 12 ++++-----
 tests/lean/run/e16.lean                 | 12 ++++-----
 tests/lean/run/e17.lean                 | 12 ++++-----
 tests/lean/run/e18.lean                 | 12 ++++-----
 tests/lean/run/e5.lean                  |  4 +--
 tests/lean/run/enum.lean                |  6 ++---
 tests/lean/run/eq1.lean                 |  2 +-
 tests/lean/run/eq10.lean                | 12 ++++-----
 tests/lean/run/eq11.lean                |  2 +-
 tests/lean/run/eq21.lean                |  4 +--
 tests/lean/run/eq23.lean                |  8 +++---
 tests/lean/run/eq24.lean                |  8 +++---
 tests/lean/run/eq25.lean                |  4 +--
 tests/lean/run/example1.lean            |  2 +-
 tests/lean/run/finbug.lean              |  4 +--
 tests/lean/run/finbug2.lean             |  4 +--
 tests/lean/run/forest.lean              |  6 ++---
 tests/lean/run/forest2.lean             | 18 ++++++-------
 tests/lean/run/forest_height.lean       |  6 ++---
 tests/lean/run/ftree_brec.lean          |  4 +--
 tests/lean/run/ho.lean                  |  4 +--
 tests/lean/run/ind0.lean                |  4 +--
 tests/lean/run/ind1.lean                |  4 +--
 tests/lean/run/ind2.lean                |  8 +++---
 tests/lean/run/ind3.lean                |  6 ++---
 tests/lean/run/ind4.lean                | 10 ++++----
 tests/lean/run/ind5.lean                |  4 +--
 tests/lean/run/ind6.lean                |  6 ++---
 tests/lean/run/ind7.lean                |  4 +--
 tests/lean/run/ind_ns.lean              |  2 +-
 tests/lean/run/indimp.lean              | 12 ++++-----
 tests/lean/run/induniv.lean             | 14 +++++-----
 tests/lean/run/inf_tree.lean            |  4 +--
 tests/lean/run/inf_tree2.lean           |  8 +++---
 tests/lean/run/inf_tree3.lean           |  8 +++---
 tests/lean/run/inv_bug.lean             |  6 ++---
 tests/lean/run/is_nil.lean              |  4 +--
 tests/lean/run/list_elab1.lean          |  4 +--
 tests/lean/run/nat_bug.lean             |  4 +--
 tests/lean/run/nat_bug2.lean            |  4 +--
 tests/lean/run/nat_bug3.lean            |  4 +--
 tests/lean/run/nat_bug4.lean            |  4 +--
 tests/lean/run/nat_bug5.lean            |  4 +--
 tests/lean/run/nat_bug6.lean            |  4 +--
 tests/lean/run/nat_bug7.lean            |  4 +--
 tests/lean/run/nested_begin.lean        |  4 +--
 tests/lean/run/no_confusion_bug.lean    |  8 +++---
 tests/lean/run/one2.lean                |  4 +--
 tests/lean/run/opaque_hint_bug.lean     |  4 +--
 tests/lean/run/record1.lean             |  2 +-
 tests/lean/run/record3.lean             |  2 +-
 tests/lean/run/record4.lean             |  2 +-
 tests/lean/run/secnot.lean              |  4 +--
 tests/lean/run/structure_test.lean      |  2 +-
 tests/lean/run/sum_bug.lean             |  4 +--
 tests/lean/run/tactic23.lean            |  4 +--
 tests/lean/run/tactic26.lean            |  4 +--
 tests/lean/run/tactic28.lean            |  4 +--
 tests/lean/run/tree.lean                |  4 +--
 tests/lean/run/tree2.lean               |  4 +--
 tests/lean/run/tree3.lean               |  4 +--
 tests/lean/run/tree_height.lean         |  4 +--
 tests/lean/run/tree_subterm_pred.lean   |  8 +++---
 tests/lean/run/uni.lean                 |  4 +--
 tests/lean/run/uni2.lean                |  4 +--
 tests/lean/run/uni_issue1.lean          |  4 +--
 tests/lean/run/univ_problem.lean        |  4 +--
 tests/lean/run/uuu.lean                 |  8 +++---
 tests/lean/run/vars_anywhere.lean       |  4 +--
 tests/lean/run/vec_inv.lean             |  4 +--
 tests/lean/run/vec_inv2.lean            |  4 +--
 tests/lean/run/vec_inv3.lean            |  4 +--
 tests/lean/run/vector.lean              |  4 +--
 tests/lean/run/vector2.lean             |  4 +--
 tests/lean/run/vector3.lean             |  4 +--
 tests/lean/run/vector_subterm_pred.lean |  4 +--
 tests/lean/slow/list_elab2.lean         |  4 +--
 tests/lean/slow/nat_bug1.lean           |  4 +--
 tests/lean/slow/nat_bug2.lean           |  4 +--
 tests/lean/slow/nat_wo_hints.lean       |  4 +--
 127 files changed, 345 insertions(+), 339 deletions(-)

diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 6a8b2fb93..b9fa335ec 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -36,8 +36,8 @@ structure prod (A B : Type) :=
 mk :: (pr1 : A) (pr2 : B)
 
 inductive sum (A B : Type) : Type :=
-inl {} : A → sum A B,
-inr {} : B → sum A B
+| inl {} : A → sum A B
+| inr {} : B → sum A B
 
 definition sum.intro_left [reducible] {A : Type} (B : Type) (a : A) : sum A B :=
 sum.inl a
@@ -49,29 +49,29 @@ sum.inr b
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
 inductive pos_num : Type :=
-one  : pos_num,
-bit1 : pos_num → pos_num,
-bit0 : pos_num → pos_num
+| one  : pos_num
+| bit1 : pos_num → pos_num
+| bit0 : pos_num → pos_num
 
 inductive num : Type :=
-zero  : num,
-pos   : pos_num → num
+| zero  : num
+| pos   : pos_num → num
 
 inductive bool : Type :=
-ff : bool,
-tt : bool
+| ff : bool
+| tt : bool
 
 inductive char : Type :=
 mk : bool → bool → bool → bool → bool → bool → bool → bool → char
 
 inductive string : Type :=
-empty : string,
-str   : char → string → string
+| empty : string
+| str   : char → string → string
 
 inductive nat :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 inductive option (A : Type) : Type :=
-none {} : option A,
-some    : A → option A
+| none {} : option A
+| some    : A → option A
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index f0e3091d0..655b148ec 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -199,8 +199,8 @@ end inhabited
 /- decidable -/
 
 inductive decidable.{l} [class] (p : Type.{l}) : Type.{l} :=
-inl :  p → decidable p,
-inr : ¬p → decidable p
+| inl :  p → decidable p
+| inr : ¬p → decidable p
 
 namespace decidable
   variables {p q : Type}
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index a1c357251..e222316dc 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -14,8 +14,8 @@ namespace nat
   notation `ℕ` := nat
 
   inductive lt (a : nat) : nat → Type :=
-  base : lt a (succ a),
-  step : Π {b}, lt a b → lt a (succ b)
+  | base : lt a (succ a)
+  | step : Π {b}, lt a b → lt a (succ b)
 
   notation a < b := lt a b
 
diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean
index a175be5b8..c7ef20ae0 100644
--- a/hott/init/relation.hlean
+++ b/hott/init/relation.hlean
@@ -38,5 +38,5 @@ definition inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive
 λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁
 
 inductive tc {A : Type} (R : A → A → Type) : A → A → Type :=
-base  : ∀a b, R a b → tc R a b,
-trans : ∀a b c, tc R a b → tc R b c → tc R a c
+| base  : ∀a b, R a b → tc R a b
+| trans : ∀a b c, tc R a b → tc R b c → tc R a c
diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index 713dbc31e..fa8b79600 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -67,8 +67,8 @@ opaque definition inversion  (id : expr)  : tactic := builtin
 notation a `↦` b:max := rename a b
 
 inductive expr_list : Type :=
-nil  : expr_list,
-cons : expr → expr_list → expr_list
+| nil  : expr_list
+| cons : expr → expr_list → expr_list
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index f5ac3a532..e3d5b72ab 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -21,8 +21,8 @@ open eq nat sigma unit
 namespace is_trunc
 
   inductive trunc_index : Type₁ :=
-  minus_two : trunc_index,
-  succ : trunc_index → trunc_index
+  | minus_two : trunc_index
+  | succ : trunc_index → trunc_index
 
   /-
      notation for trunc_index is -2, -1, 0, 1, ...
diff --git a/hott/init/types/prod.hlean b/hott/init/types/prod.hlean
index 407c55265..4df8007d2 100644
--- a/hott/init/types/prod.hlean
+++ b/hott/init/types/prod.hlean
@@ -47,8 +47,8 @@ namespace prod
 
   -- Lexicographical order based on Ra and Rb
   inductive lex : A × B → A × B → Type :=
-  left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂),
-  right : ∀a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
+  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
+  | right : ∀a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
 
   -- Relational product based on Ra and Rb
   inductive rprod : A × B → A × B → Type :=
diff --git a/library/data/fin.lean b/library/data/fin.lean
index fea0d20aa..bfbe0b417 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -11,8 +11,8 @@ import data.nat
 open nat
 
 inductive fin : nat → Type :=
-fz : Π n, fin (succ n),
-fs : Π {n}, fin n → fin (succ n)
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
   definition to_nat : Π {n}, fin n → nat
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 6a8fdf317..2ef85ad1c 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -37,8 +37,8 @@ open decidable binary fake_simplifier
 /- the type of integers -/
 
 inductive int : Type :=
-  of_nat : nat → int,
-  neg_succ_of_nat : nat → int
+| of_nat : nat → int
+| neg_succ_of_nat : nat → int
 
 notation `ℤ` := int
 attribute int.of_nat [coercion]
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 2d4fef642..1496a250a 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -13,8 +13,8 @@ import logic tools.helper_tactics data.nat.basic
 open eq.ops helper_tactics nat
 
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons   : T → list T → list T
+| nil {} : list T
+| cons   : T → list T → list T
 
 namespace list
 notation h :: t  := cons h t
diff --git a/library/data/vector.lean b/library/data/vector.lean
index 8fe141fcc..d537bc249 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -9,8 +9,8 @@ import data.nat.basic
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
-  nil {} : vector A zero,
-  cons   : Π {n}, A → vector A n → vector A (succ n)
+| nil {} : vector A zero
+| cons   : Π {n}, A → vector A n → vector A (succ n)
 
 namespace vector
   notation a :: b := cons a b
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 814626fb1..84088a3e4 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -50,8 +50,8 @@ and.rec (λa b, b) H
 definition and.right := @and.elim_right
 
 inductive sum (A B : Type) : Type :=
-inl {} : A → sum A B,
-inr {} : B → sum A B
+| inl {} : A → sum A B
+| inr {} : B → sum A B
 
 definition sum.intro_left [reducible] {A : Type} (B : Type) (a : A) : sum A B :=
 sum.inl a
@@ -60,8 +60,8 @@ definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B :
 sum.inr b
 
 inductive or (a b : Prop) : Prop :=
-inl {} : a → or a b,
-inr {} : b → or a b
+| inl {} : a → or a b
+| inr {} : b → or a b
 
 definition or.intro_left {a : Prop} (b : Prop) (Ha : a) : or a b :=
 or.inl Ha
@@ -76,9 +76,9 @@ mk :: (pr1 : A) (pr2 : B pr1)
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
 inductive pos_num : Type :=
-one  : pos_num,
-bit1 : pos_num → pos_num,
-bit0 : pos_num → pos_num
+| one  : pos_num
+| bit1 : pos_num → pos_num
+| bit0 : pos_num → pos_num
 
 namespace pos_num
   definition succ (a : pos_num) : pos_num :=
@@ -86,8 +86,8 @@ namespace pos_num
 end pos_num
 
 inductive num : Type :=
-zero  : num,
-pos   : pos_num → num
+| zero  : num
+| pos   : pos_num → num
 
 namespace num
   open pos_num
@@ -96,20 +96,20 @@ namespace num
 end num
 
 inductive bool : Type :=
-ff : bool,
-tt : bool
+| ff : bool
+| tt : bool
 
 inductive char : Type :=
 mk : bool → bool → bool → bool → bool → bool → bool → bool → char
 
 inductive string : Type :=
-empty : string,
-str   : char → string → string
+| empty : string
+| str   : char → string → string
 
 inductive nat :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 inductive option (A : Type) : Type :=
-none {} : option A,
-some    : A → option A
+| none {} : option A
+| some    : A → option A
diff --git a/library/init/logic.lean b/library/init/logic.lean
index b2cf2b005..13becad16 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -241,8 +241,8 @@ theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2
 Exists.rec H2 H1
 
 inductive decidable [class] (p : Prop) : Type :=
-inl :  p → decidable p,
-inr : ¬p → decidable p
+| inl :  p → decidable p
+| inr : ¬p → decidable p
 
 definition decidable_true [instance] : decidable true :=
 decidable.inl trivial
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 62c3a78dc..b162d8f92 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -14,8 +14,8 @@ namespace nat
   notation `ℕ` := nat
 
   inductive lt (a : nat) : nat → Prop :=
-  base : lt a (succ a),
-  step : Π {b}, lt a b → lt a (succ b)
+  | base : lt a (succ a)
+  | step : Π {b}, lt a b → lt a (succ b)
 
   notation a < b := lt a b
 
diff --git a/library/init/prod.lean b/library/init/prod.lean
index 02be42cb4..a515e9bcb 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -38,8 +38,8 @@ namespace prod
 
   -- Lexicographical order based on Ra and Rb
   inductive lex : A × B → A × B → Prop :=
-  left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂),
-  right : ∀a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
+  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
+  | right : ∀a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
 
   -- Relational product based on Ra and Rb
   inductive rprod : A × B → A × B → Prop :=
diff --git a/library/init/relation.lean b/library/init/relation.lean
index 0477ab330..c2b4b18f4 100644
--- a/library/init/relation.lean
+++ b/library/init/relation.lean
@@ -38,5 +38,5 @@ theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (i
 λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁
 
 inductive tc {A : Type} (R : A → A → Prop) : A → A → Prop :=
-base  : ∀a b, R a b → tc R a b,
-trans : ∀a b c, tc R a b → tc R b c → tc R a c
+| base  : ∀a b, R a b → tc R a b
+| trans : ∀a b c, tc R a b → tc R b c → tc R a c
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 1692d22f7..419d53e1c 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -31,8 +31,8 @@ namespace sigma
 
   -- Lexicographical order based on Ra and Rb
   inductive lex : sigma B → sigma B → Prop :=
-  left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
-  right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex ⟨a, b₁⟩  ⟨a, b₂⟩
+  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
+  | right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex ⟨a, b₁⟩  ⟨a, b₂⟩
   end
 
   context
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index ad45956ac..490955979 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -67,8 +67,8 @@ opaque definition inversion  (id : expr)  : tactic := builtin
 notation a `↦` b:max := rename a b
 
 inductive expr_list : Type :=
-nil  : expr_list,
-cons : expr → expr_list → expr_list
+| nil  : expr_list
+| cons : expr → expr_list → expr_list
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index ab3ff8606..2c9a52a92 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -234,6 +234,10 @@ struct inductive_cmd_fn {
             m_p.add_local(l);
     }
 
+    bool curr_is_intro_prefix() const {
+        return m_p.curr_is_token(get_bar_tk()) || m_p.curr_is_token(get_comma_tk());
+    }
+
     /** \brief Parse introduction rules in the scope of m_params.
 
         Introduction rules with the annotation '{}' are marked for relaxed (aka non-strict) implicit parameter inference.
@@ -241,6 +245,8 @@ struct inductive_cmd_fn {
     */
     list<intro_rule> parse_intro_rules(name const & ind_name) {
         buffer<intro_rule> intros;
+        if (m_p.curr_is_token(get_bar_tk()))
+            m_p.next();
         while (true) {
             name intro_name = parse_intro_decl_name(ind_name);
             implicit_infer_kind k = parse_implicit_infer_modifier(m_p);
@@ -253,7 +259,7 @@ struct inductive_cmd_fn {
                 expr intro_type = mk_constant(ind_name);
                 intros.push_back(intro_rule(intro_name, intro_type));
             }
-            if (!m_p.curr_is_token(get_comma_tk()))
+            if (!curr_is_intro_prefix())
                 break;
             m_p.next();
         }
diff --git a/tests/lean/K_bug.lean b/tests/lean/K_bug.lean
index e0743cd33..0e56a3bb7 100644
--- a/tests/lean/K_bug.lean
+++ b/tests/lean/K_bug.lean
@@ -1,7 +1,7 @@
 open eq.ops
 
 inductive Nat : Type :=
-zero : Nat,
+zero : Nat |
 succ : Nat → Nat
 
 namespace Nat
diff --git a/tests/lean/bad_eqns.lean b/tests/lean/bad_eqns.lean
index 24d97036a..f437578ab 100644
--- a/tests/lean/bad_eqns.lean
+++ b/tests/lean/bad_eqns.lean
@@ -12,11 +12,11 @@ definition foo : nat → nat → nat
 | foo ⌞x⌟ x := x
 
 inductive tree (A : Type) :=
-node   : tree_list A → tree A,
-leaf   : A → tree A
+| node   : tree_list A → tree A
+| leaf   : A → tree A
 with tree_list :=
-nil {} : tree_list A,
-cons   : tree A → tree_list A → tree_list A
+| nil {} : tree_list A
+| cons   : tree A → tree_list A → tree_list A
 
 definition is_leaf {A : Type} : tree A → bool
 with is_leaf_aux : tree_list A → bool
diff --git a/tests/lean/error_full_names.lean b/tests/lean/error_full_names.lean
index f3e13c23c..04e7d86c1 100644
--- a/tests/lean/error_full_names.lean
+++ b/tests/lean/error_full_names.lean
@@ -1,6 +1,6 @@
 namespace foo
 open nat
-inductive nat : Type := zero, foosucc : nat → nat
+inductive nat : Type := zero | foosucc : nat → nat
 check 0 + nat.zero --error
 end foo
 
diff --git a/tests/lean/ftree.lean b/tests/lean/ftree.lean
index 8d6264871..2ec6f1b72 100644
--- a/tests/lean/ftree.lean
+++ b/tests/lean/ftree.lean
@@ -1,10 +1,10 @@
-inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T
+inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T
 
 namespace explicit
 
 inductive ftree.{l₁ l₂} (A : Type.{l₁}) (B : Type.{l₂}) : Type.{max 1 l₁ l₂} :=
-leafa : A → ftree A B,
-leafb : B → ftree A B,
+leafa : A → ftree A B |
+leafb : B → ftree A B |
 node  : (A → ftree A B) → (B → ftree A B) → ftree A B
 
 end explicit
@@ -12,7 +12,7 @@ end explicit
 namespace implicit
 
 inductive ftree (A : Type) (B : Type) : Type :=
-leafa : ftree A B,
+leafa : ftree A B |
 node  : (A → B → ftree A B) → (B → ftree A B) → ftree A B
 
 set_option pp.universes true
@@ -23,8 +23,8 @@ end implicit
 namespace implicit2
 
 inductive ftree (A : Type) (B : Type) : Type :=
-leafa : A → ftree A B,
-leafb : B → ftree A B,
+leafa : A → ftree A B |
+leafb : B → ftree A B |
 node  : (list A → ftree A B) → (B → ftree A B) → ftree A B
 
 check ftree
diff --git a/tests/lean/hott/cases.hlean b/tests/lean/hott/cases.hlean
index bfad630b2..7e2b52688 100644
--- a/tests/lean/hott/cases.hlean
+++ b/tests/lean/hott/cases.hlean
@@ -1,8 +1,8 @@
 open nat
 
 inductive vec (A : Type) : nat → Type :=
-nil {} : vec A zero,
-cons   : Π {n}, A → vec A n → vec A (succ n)
+| nil {} : vec A zero
+| cons   : Π {n}, A → vec A n → vec A (succ n)
 
 namespace vec
   variables {A B C : Type}
diff --git a/tests/lean/hott/eq1.hlean b/tests/lean/hott/eq1.hlean
index db5913e40..e29f0cda2 100644
--- a/tests/lean/hott/eq1.hlean
+++ b/tests/lean/hott/eq1.hlean
@@ -1,8 +1,8 @@
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-nil {} : vector A zero,
-cons   : Π {n}, A → vector A n → vector A (succ n)
+| nil {} : vector A zero
+| cons   : Π {n}, A → vector A n → vector A (succ n)
 
 infixr `::` := vector.cons
 
diff --git a/tests/lean/hott/inv_bug.hlean b/tests/lean/hott/inv_bug.hlean
index 3e1ac2b6d..b154d50b3 100644
--- a/tests/lean/hott/inv_bug.hlean
+++ b/tests/lean/hott/inv_bug.hlean
@@ -2,10 +2,10 @@ open nat
 open eq.ops
 
 inductive even : nat → Type :=
-even_zero        : even zero,
-even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
+| even_zero        : even zero
+| even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
 with odd : nat → Type :=
-odd_succ_of_even : ∀ {a}, even a → odd (succ a)
+| odd_succ_of_even : ∀ {a}, even a → odd (succ a)
 
 example : even 1 → empty :=
 begin
diff --git a/tests/lean/hott/noc_list.hlean b/tests/lean/hott/noc_list.hlean
index c31b66c7a..be7ff50f8 100644
--- a/tests/lean/hott/noc_list.hlean
+++ b/tests/lean/hott/noc_list.hlean
@@ -1,6 +1,6 @@
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 
 namespace list
   open lift
diff --git a/tests/lean/hott/tele.hlean b/tests/lean/hott/tele.hlean
index 59fe8c193..26e09589c 100644
--- a/tests/lean/hott/tele.hlean
+++ b/tests/lean/hott/tele.hlean
@@ -5,8 +5,8 @@
 open nat
 
 inductive vec (A : Type) : nat → Type :=
-nil {} : vec A zero,
-cons   : Π {n}, A → vec A n → vec A (succ n)
+| nil {} : vec A zero
+| cons   : Π {n}, A → vec A n → vec A (succ n)
 
 structure S (A : Type) (a : A) (n : nat) (v : vec A n) :=
 mk :: (fa : A)
diff --git a/tests/lean/interactive/auto_comp.input b/tests/lean/interactive/auto_comp.input
index 9e4a44f08..489285267 100644
--- a/tests/lean/interactive/auto_comp.input
+++ b/tests/lean/interactive/auto_comp.input
@@ -1,8 +1,8 @@
 VISIT auto_comp.lean
 SYNC 8
 prelude
-inductive nat  := zero : nat, succ : nat → nat
-inductive bool := ff, tt
+inductive nat  := zero : nat | succ : nat → nat
+inductive bool := ff | tt
 namespace nat
   inductive le : nat → nat → Type.{0} := refl : Π a, le a a
 
diff --git a/tests/lean/interactive/extra_type.input b/tests/lean/interactive/extra_type.input
index b1c3006ff..fb42ac088 100644
--- a/tests/lean/interactive/extra_type.input
+++ b/tests/lean/interactive/extra_type.input
@@ -7,10 +7,10 @@ definition Prop := Type.{0}
 inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a
 infix `=`:50 := eq
 definition rfl {A : Type} {a : A} := eq.refl a
-inductive or (A B : Prop) : Prop := inl {} : A → or A B, inr {} : B → or A B
+inductive or (A B : Prop) : Prop := inl {} : A → or A B | inr {} : B → or A B
 infix `∨`:35 := or
 inductive bool : Type :=
-  ff : bool,
+  ff : bool|
   tt : bool
 namespace bool
   protected definition rec_on2 {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
diff --git a/tests/lean/interactive/missing.lean b/tests/lean/interactive/missing.lean
index 1136a21b1..11cf75504 100644
--- a/tests/lean/interactive/missing.lean
+++ b/tests/lean/interactive/missing.lean
@@ -1,7 +1,7 @@
 import logic
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
+leaf : A → tree A|
 node : tree A → tree A → tree A
 
 namespace tree
diff --git a/tests/lean/interactive/num2.lean b/tests/lean/interactive/num2.lean
index 21342523a..06c5e0227 100644
--- a/tests/lean/interactive/num2.lean
+++ b/tests/lean/interactive/num2.lean
@@ -9,8 +9,8 @@ import logic.inhabited
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
 inductive pos_num : Type :=
-one  : pos_num,
-bit1 : pos_num → pos_num,
+one  : pos_num|
+bit1 : pos_num → pos_num|
 bit0 : pos_num → pos_num
 
 theorem pos_num.is_inhabited [instance] : inhabited pos_num :=
diff --git a/tests/lean/inv_del.lean b/tests/lean/inv_del.lean
index 4cfca0bce..06f7ca346 100644
--- a/tests/lean/inv_del.lean
+++ b/tests/lean/inv_del.lean
@@ -2,8 +2,8 @@ import logic
 open nat
 
 inductive vec (A : Type) : nat → Type :=
-vnil : vec A zero,
-vone : A → vec A (succ zero),
+vnil : vec A zero |
+vone : A → vec A (succ zero) |
 vtwo : A → A → vec A (succ (succ zero))
 
 namespace vec
diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean
index 3087f4624..da9ba3431 100644
--- a/tests/lean/no_confusion_type.lean
+++ b/tests/lean/no_confusion_type.lean
@@ -2,7 +2,7 @@ import logic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
+vnil  : vector A zero |
 vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 check vector.no_confusion_type
diff --git a/tests/lean/notation2.lean b/tests/lean/notation2.lean
index 25372a356..a1c631b1c 100644
--- a/tests/lean/notation2.lean
+++ b/tests/lean/notation2.lean
@@ -1,5 +1,5 @@
 import data.num
-inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 infixr `::` := cons
 check 1 :: 2 :: nil
 check 1 :: 2 :: 3 :: 4 :: 5 :: nil
diff --git a/tests/lean/notation3.lean b/tests/lean/notation3.lean
index 6e82b417c..65def3ce7 100644
--- a/tests/lean/notation3.lean
+++ b/tests/lean/notation3.lean
@@ -1,5 +1,5 @@
 import data.prod data.num
-inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 open prod num
 constants a b : num
 check [a, b, b]
diff --git a/tests/lean/notation4.lean b/tests/lean/notation4.lean
index 5f63b2ee6..0f1dffeab 100644
--- a/tests/lean/notation4.lean
+++ b/tests/lean/notation4.lean
@@ -1,6 +1,6 @@
 import logic data.sigma
 open sigma
-inductive list (T : Type) : Type := nil {} : list T, cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check ∃ (A : Type₁) (x y : A), x = y
 check ∃ (x : num), x = 0
 check Σ (x : num), x = 10
diff --git a/tests/lean/proj.lean b/tests/lean/proj.lean
index 5ab3f8ebd..d4babaa0b 100644
--- a/tests/lean/proj.lean
+++ b/tests/lean/proj.lean
@@ -1,8 +1,8 @@
 import logic
 
 inductive vector (T : Type) : nat → Type :=
-  nil {} : vector T nat.zero,
-  cons : T → ∀{n}, vector T n → vector T (nat.succ n)
+| nil {} : vector T nat.zero
+| cons : T → ∀{n}, vector T n → vector T (nat.succ n)
 
 #projections or
 #projections and
diff --git a/tests/lean/run/331.lean b/tests/lean/run/331.lean
index ad3188d6e..7a92864d6 100644
--- a/tests/lean/run/331.lean
+++ b/tests/lean/run/331.lean
@@ -1,7 +1,7 @@
 namespace nat
   inductive less (a : nat) : nat → Prop :=
-  base : less a (succ a),
-  step : Π {b}, less a b → less a (succ b)
+  | base : less a (succ a)
+  | step : Π {b}, less a b → less a (succ b)
 
 end nat
 
diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean
index 628e4209e..0ecdef98a 100644
--- a/tests/lean/run/algebra1.lean
+++ b/tests/lean/run/algebra1.lean
@@ -35,8 +35,8 @@ end algebra
 
 open algebra
   inductive nat : Type :=
-  zero : nat,
-  succ : nat → nat
+  | zero : nat
+  | succ : nat → nat
 
 namespace nat
 
diff --git a/tests/lean/run/alias3.lean b/tests/lean/run/alias3.lean
index 18c9b9608..b5e7f914b 100644
--- a/tests/lean/run/alias3.lean
+++ b/tests/lean/run/alias3.lean
@@ -17,8 +17,8 @@ namespace N2
   context
     parameter A : Type
     inductive list : Type :=
-    nil {} : list,
-    cons   : A → list → list
+    | nil {} : list
+    | cons   : A → list → list
     check list
   end
   check list
diff --git a/tests/lean/run/cast_sorry_bug.lean b/tests/lean/run/cast_sorry_bug.lean
index 858969af8..37804762e 100644
--- a/tests/lean/run/cast_sorry_bug.lean
+++ b/tests/lean/run/cast_sorry_bug.lean
@@ -2,8 +2,8 @@ import logic data.nat
 open nat
 
 inductive fin : ℕ → Type :=
-zero : Π {n : ℕ}, fin (succ n),
-succ : Π {n : ℕ}, fin n → fin (succ n)
+| zero : Π {n : ℕ}, fin (succ n)
+| succ : Π {n : ℕ}, fin n → fin (succ n)
 
 theorem foo (n m : ℕ) (a : fin n) (b : fin m) (H : n = m) : cast (congr_arg fin H) a = b :=
 have eq  : fin n = fin m, from congr_arg fin H,
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index c18f91f0d..c66da2bd2 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -2,8 +2,8 @@ prelude
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 open eq
 
diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean
index dc53242e1..b84395a0d 100644
--- a/tests/lean/run/class5.lean
+++ b/tests/lean/run/class5.lean
@@ -13,8 +13,8 @@ end algebra
 open algebra
 namespace nat
   inductive nat : Type :=
-  zero : nat,
-  succ : nat → nat
+  | zero : nat
+  | succ : nat → nat
 
   constant mul : nat → nat → nat
   constant add : nat → nat → nat
diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean
index 6698eab4d..ea842448c 100644
--- a/tests/lean/run/coercion_bug2.lean
+++ b/tests/lean/run/coercion_bug2.lean
@@ -2,8 +2,8 @@ import data.nat
 open nat
 
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons : T → list T → list T
+| nil {} : list T
+| cons : T → list T → list T
 
 definition length {T : Type} : list T → nat := list.rec 0 (fun x l m, succ m)
 theorem length_nil {T : Type} : length (@list.nil T) = 0
diff --git a/tests/lean/run/confuse_ind.lean b/tests/lean/run/confuse_ind.lean
index 6df5c3a42..cad894350 100644
--- a/tests/lean/run/confuse_ind.lean
+++ b/tests/lean/run/confuse_ind.lean
@@ -4,8 +4,8 @@ definition mk_arrow (A : Type) (B : Type) :=
 A → A → B
 
 inductive confuse (A : Type) :=
-leaf1 : confuse A,
-leaf2 : num → confuse A,
-node : mk_arrow A (confuse A) → confuse A
+| leaf1 : confuse A
+| leaf2 : num → confuse A
+| node : mk_arrow A (confuse A) → confuse A
 
 check confuse.cases_on
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index c70cb9e19..7bf29c15b 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -1,12 +1,12 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat end nat open nat
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 definition nil := @list.nil
 definition cons := @list.cons
 
@@ -18,8 +18,8 @@ check @nil nat
 check cons nat.zero nil
 
 inductive vector (A : Type) : nat → Type :=
-vnil {} : vector A zero,
-vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+| vnil {} : vector A zero
+| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean
index 3ef931c2f..280635eb4 100644
--- a/tests/lean/run/e15.lean
+++ b/tests/lean/run/e15.lean
@@ -1,12 +1,12 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat end nat open nat
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 namespace list end list open list
 check nil
 check nil.{1}
@@ -16,8 +16,8 @@ check @nil nat
 check cons zero nil
 
 inductive vector (A : Type) : nat → Type :=
-vnil {} : vector A zero,
-vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+| vnil {} : vector A zero
+| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean
index 2df9ba0c0..b9979b5bc 100644
--- a/tests/lean/run/e16.lean
+++ b/tests/lean/run/e16.lean
@@ -1,12 +1,12 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat end nat open nat
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 namespace list end list open list
 
 check nil
@@ -17,8 +17,8 @@ check @nil nat
 check cons zero nil
 
 inductive vector (A : Type) : nat → Type :=
-vnil {} : vector A zero,
-vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
+| vnil {} : vector A zero
+| vcons   : forall {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 
 check vcons zero vnil
diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean
index 1ddcf77f2..91691e26f 100644
--- a/tests/lean/run/e17.lean
+++ b/tests/lean/run/e17.lean
@@ -1,15 +1,15 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 
 inductive int : Type :=
-of_nat : nat → int,
-neg : nat → int
+| of_nat : nat → int
+| neg : nat → int
 
 attribute int.of_nat [coercion]
 
diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
index a9f55a97a..011dc49db 100644
--- a/tests/lean/run/e18.lean
+++ b/tests/lean/run/e18.lean
@@ -1,15 +1,15 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 
 inductive int : Type :=
-of_nat : nat → int,
-neg : nat → int
+| of_nat : nat → int
+| neg : nat → int
 
 attribute int.of_nat [coercion]
 
diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean
index 9634f54e7..559ea6fd3 100644
--- a/tests/lean/run/e5.lean
+++ b/tests/lean/run/e5.lean
@@ -33,8 +33,8 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
 := subst H2 H1
 
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat end nat open nat
 
 print "using strict implicit arguments"
diff --git a/tests/lean/run/enum.lean b/tests/lean/run/enum.lean
index 306a4d7f7..77b9899e0 100644
--- a/tests/lean/run/enum.lean
+++ b/tests/lean/run/enum.lean
@@ -1,9 +1,9 @@
 import logic
 
 inductive Three :=
-zero : Three,
-one  : Three,
-two  : Three
+| zero : Three
+| one  : Three
+| two  : Three
 
 namespace Three
 
diff --git a/tests/lean/run/eq1.lean b/tests/lean/run/eq1.lean
index 8f278dd5a..cc0396146 100644
--- a/tests/lean/run/eq1.lean
+++ b/tests/lean/run/eq1.lean
@@ -1,5 +1,5 @@
 inductive day :=
-monday, tuesday, wednesday, thursday, friday, saturday, sunday
+monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
 open day
 
diff --git a/tests/lean/run/eq10.lean b/tests/lean/run/eq10.lean
index f87832c01..1c48b3756 100644
--- a/tests/lean/run/eq10.lean
+++ b/tests/lean/run/eq10.lean
@@ -1,10 +1,10 @@
 inductive formula :=
-eqf  : nat → nat → formula,
-andf : formula → formula → formula,
-impf : formula → formula → formula,
-notf : formula → formula,
-orf  : formula → formula → formula,
-allf : (nat → formula) → formula
+| eqf  : nat → nat → formula
+| andf : formula → formula → formula
+| impf : formula → formula → formula
+| notf : formula → formula
+| orf  : formula → formula → formula
+| allf : (nat → formula) → formula
 
 namespace formula
   definition implies (a b : Prop) : Prop := a → b
diff --git a/tests/lean/run/eq11.lean b/tests/lean/run/eq11.lean
index a15ab186f..08b7b383a 100644
--- a/tests/lean/run/eq11.lean
+++ b/tests/lean/run/eq11.lean
@@ -1,5 +1,5 @@
 inductive day :=
-monday, tuesday, wednesday, thursday, friday, saturday, sunday
+monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
 open day
 
diff --git a/tests/lean/run/eq21.lean b/tests/lean/run/eq21.lean
index e61c2b491..00afa15c6 100644
--- a/tests/lean/run/eq21.lean
+++ b/tests/lean/run/eq21.lean
@@ -1,6 +1,6 @@
 inductive formula :=
-eqf  : nat → nat → formula,
-impf : formula → formula → formula
+| eqf  : nat → nat → formula
+| impf : formula → formula → formula
 
 namespace formula
   definition denote : formula → Prop
diff --git a/tests/lean/run/eq23.lean b/tests/lean/run/eq23.lean
index 1c4afcaee..75419afbe 100644
--- a/tests/lean/run/eq23.lean
+++ b/tests/lean/run/eq23.lean
@@ -1,11 +1,11 @@
 open nat
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree_list A → tree A
+| leaf : A → tree A
+| node : tree_list A → tree A
 with tree_list :=
-nil  : tree_list A,
-cons : tree A → tree_list A → tree_list A
+| nil  : tree_list A
+| cons : tree A → tree_list A → tree_list A
 
 namespace tree_list
 
diff --git a/tests/lean/run/eq24.lean b/tests/lean/run/eq24.lean
index b827e8e60..9f1ac48f7 100644
--- a/tests/lean/run/eq24.lean
+++ b/tests/lean/run/eq24.lean
@@ -1,11 +1,11 @@
 open nat
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree_list A → tree A
+| leaf : A → tree A
+| node : tree_list A → tree A
 with tree_list :=
-nil  : tree_list A,
-cons : tree A → tree_list A → tree_list A
+| nil  : tree_list A
+| cons : tree A → tree_list A → tree_list A
 
 namespace tree
 open tree_list
diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean
index 2768472f0..6ec2f1648 100644
--- a/tests/lean/run/eq25.lean
+++ b/tests/lean/run/eq25.lean
@@ -1,6 +1,6 @@
 inductive N :=
-O : N,
-S : N → N
+| O : N
+| S : N → N
 
 definition Nat := N
 
diff --git a/tests/lean/run/example1.lean b/tests/lean/run/example1.lean
index 4ff3cb4db..87393445b 100644
--- a/tests/lean/run/example1.lean
+++ b/tests/lean/run/example1.lean
@@ -1,7 +1,7 @@
 import logic
 
 inductive day :=
-monday, tuesday, wednesday, thursday, friday, saturday, sunday
+monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
 namespace day
 
diff --git a/tests/lean/run/finbug.lean b/tests/lean/run/finbug.lean
index c1819b2bd..5ddec75d0 100644
--- a/tests/lean/run/finbug.lean
+++ b/tests/lean/run/finbug.lean
@@ -10,8 +10,8 @@ Finite ordinals.
 open nat
 
 inductive fin : nat → Type :=
-fz : Π n, fin (succ n),
-fs : Π {n}, fin n → fin (succ n)
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
   definition to_nat : Π {n}, fin n → nat
diff --git a/tests/lean/run/finbug2.lean b/tests/lean/run/finbug2.lean
index cc8978177..31c3a3233 100644
--- a/tests/lean/run/finbug2.lean
+++ b/tests/lean/run/finbug2.lean
@@ -10,8 +10,8 @@ Finite ordinals.
 open nat
 
 inductive fin : nat → Type :=
-fz : Π n, fin (succ n),
-fs : Π {n}, fin n → fin (succ n)
+| fz : Π n, fin (succ n)
+| fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
   definition to_nat : Π {n}, fin n → nat
diff --git a/tests/lean/run/forest.lean b/tests/lean/run/forest.lean
index 3215cc578..ef0195d04 100644
--- a/tests/lean/run/forest.lean
+++ b/tests/lean/run/forest.lean
@@ -2,10 +2,10 @@ import data.prod data.unit
 open prod
 
 inductive tree (A : Type) : Type :=
-node : A → forest A → tree A
+| node : A → forest A → tree A
 with forest : Type :=
-nil  : forest A,
-cons : tree A → forest A → forest A
+| nil  : forest A
+| cons : tree A → forest A → forest A
 
 namespace manual
 definition tree.below.{l₁ l₂}
diff --git a/tests/lean/run/forest2.lean b/tests/lean/run/forest2.lean
index 82aee3f76..c348a10bf 100644
--- a/tests/lean/run/forest2.lean
+++ b/tests/lean/run/forest2.lean
@@ -2,20 +2,20 @@ import data.prod data.unit
 open prod
 
 inductive tree (A : Type) : Type :=
-node : A → forest A → tree A
+| node : A → forest A → tree A
 with forest : Type :=
-nil  : forest A,
-cons : tree A → forest A → forest A
+| nil  : forest A
+| cons : tree A → forest A → forest A
 
 namespace solution1
 
 inductive tree_forest (A : Type) :=
-of_tree   : tree A   → tree_forest A,
-of_forest : forest A → tree_forest A
+| of_tree   : tree A   → tree_forest A
+| of_forest : forest A → tree_forest A
 
 inductive same_kind {A : Type} : tree_forest A → tree_forest A → Type :=
-is_tree   : Π (t₁ t₂ : tree A),   same_kind (tree_forest.of_tree t₁)   (tree_forest.of_tree t₂),
-is_forest : Π (f₁ f₂ : forest A), same_kind (tree_forest.of_forest f₁) (tree_forest.of_forest f₂)
+| is_tree   : Π (t₁ t₂ : tree A),   same_kind (tree_forest.of_tree t₁)   (tree_forest.of_tree t₂)
+| is_forest : Π (f₁ f₂ : forest A), same_kind (tree_forest.of_forest f₁) (tree_forest.of_forest f₂)
 
 definition to_tree {A : Type} (tf : tree_forest A) (t : tree A) : same_kind tf (tree_forest.of_tree t) → tree A :=
 tree_forest.cases_on tf
@@ -29,8 +29,8 @@ namespace solution2
 variables {A B : Type}
 
 inductive same_kind : sum A B → sum A B → Prop :=
-isl : Π (a₁ a₂ : A), same_kind (sum.inl a₁) (sum.inl a₂),
-isr : Π (b₁ b₂ : B), same_kind (sum.inr b₁) (sum.inr b₂)
+| isl : Π (a₁ a₂ : A), same_kind (sum.inl a₁) (sum.inl a₂)
+| isr : Π (b₁ b₂ : B), same_kind (sum.inr b₁) (sum.inr b₂)
 
 definition to_left (s : sum A B) (a : A) : same_kind s (sum.inl a) → A :=
 sum.cases_on s
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index e045bb4ff..2ce6df042 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -2,10 +2,10 @@ import data.nat.basic data.sum data.sigma data.bool
 open nat sigma
 
 inductive tree (A : Type) : Type :=
-node : A → forest A → tree A
+| node : A → forest A → tree A
 with forest : Type :=
-nil  : forest A,
-cons : tree A → forest A → forest A
+| nil  : forest A
+| cons : tree A → forest A → forest A
 
 namespace manual
 check tree.rec_on
diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean
index 69f9f28c1..a05f61155 100644
--- a/tests/lean/run/ftree_brec.lean
+++ b/tests/lean/run/ftree_brec.lean
@@ -1,8 +1,8 @@
 import data.unit data.prod
 
 inductive ftree (A : Type) (B : Type) : Type :=
-leafa : ftree A B,
-node  : (A → B → ftree A B) → (B → ftree A B) → ftree A B
+| leafa : ftree A B
+| node  : (A → B → ftree A B) → (B → ftree A B) → ftree A B
 
 set_option pp.universes true
 check @ftree
diff --git a/tests/lean/run/ho.lean b/tests/lean/run/ho.lean
index 8daa9d9e3..bb46acc66 100644
--- a/tests/lean/run/ho.lean
+++ b/tests/lean/run/ho.lean
@@ -1,8 +1,8 @@
 import data.nat
 
 inductive star : Type₁ :=
-z  : star,
-s  : (nat → star) → star
+| z  : star
+| s  : (nat → star) → star
 
 check @star.rec
 check @star.cases_on
diff --git a/tests/lean/run/ind0.lean b/tests/lean/run/ind0.lean
index 40ac4b304..149d4ad9a 100644
--- a/tests/lean/run/ind0.lean
+++ b/tests/lean/run/ind0.lean
@@ -1,7 +1,7 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 check nat
 check nat.rec.{1}
diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean
index 2450b79c3..bac42f8f8 100644
--- a/tests/lean/run/ind1.lean
+++ b/tests/lean/run/ind1.lean
@@ -1,6 +1,6 @@
 inductive list (A : Type) : Type :=
-nil  : list A,
-cons : A → list A → list A
+| nil  : list A
+| cons : A → list A → list A
 namespace list end list open list
 check list.{1}
 check cons.{1}
diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean
index 765fbb0ab..667005111 100644
--- a/tests/lean/run/ind2.lean
+++ b/tests/lean/run/ind2.lean
@@ -1,12 +1,12 @@
 prelude
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat end nat open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
-vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil  : vector A zero
+| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 namespace vector end vector open vector
 check vector.{1}
 check vnil.{1}
diff --git a/tests/lean/run/ind3.lean b/tests/lean/run/ind3.lean
index 499b24257..950d51b2e 100644
--- a/tests/lean/run/ind3.lean
+++ b/tests/lean/run/ind3.lean
@@ -1,8 +1,8 @@
 inductive tree (A : Type) : Type :=
-node : A → forest A → tree A
+| node : A → forest A → tree A
 with forest : Type :=
-nil  : forest A,
-cons : tree A → forest A → forest A
+| nil  : forest A
+| cons : tree A → forest A → forest A
 
 
 check tree.{1}
diff --git a/tests/lean/run/ind4.lean b/tests/lean/run/ind4.lean
index e99f0c3a2..693353906 100644
--- a/tests/lean/run/ind4.lean
+++ b/tests/lean/run/ind4.lean
@@ -1,8 +1,8 @@
 section
   variable A : Type
   inductive list : Type :=
-  nil  : list,
-  cons : A → list → list
+  | nil  : list
+  | cons : A → list → list
 end
 
 check list.{1}
@@ -11,10 +11,10 @@ check list.cons.{1}
 section
   variable A : Type
   inductive tree : Type :=
-  node : A → forest → tree
+  | node : A → forest → tree
   with forest : Type :=
-  fnil  : forest,
-  fcons : tree → forest → forest
+  | fnil  : forest
+  | fcons : tree → forest → forest
   check tree
   check forest
 end
diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean
index 80bd169e8..9e3da40b1 100644
--- a/tests/lean/run/ind5.lean
+++ b/tests/lean/run/ind5.lean
@@ -2,8 +2,8 @@ prelude
 definition Prop : Type.{1} := Type.{0}
 
 inductive or (A B : Prop) : Prop :=
-intro_left  : A → or A B,
-intro_right : B → or A B
+| intro_left  : A → or A B
+| intro_right : B → or A B
 
 check or
 check or.intro_left
diff --git a/tests/lean/run/ind6.lean b/tests/lean/run/ind6.lean
index 15dbf4f06..fa213dd32 100644
--- a/tests/lean/run/ind6.lean
+++ b/tests/lean/run/ind6.lean
@@ -1,8 +1,8 @@
 inductive tree.{u} (A : Type.{u}) : Type.{max u 1} :=
-node : A → forest.{u} A → tree.{u} A
+| node : A → forest.{u} A → tree.{u} A
 with forest : Type.{max u 1} :=
-nil  : forest.{u} A,
-cons : tree.{u} A → forest.{u} A → forest.{u} A
+| nil  : forest.{u} A
+| cons : tree.{u} A → forest.{u} A → forest.{u} A
 
 check tree.{1}
 check forest.{1}
diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean
index fae5f6192..f24c7f232 100644
--- a/tests/lean/run/ind7.lean
+++ b/tests/lean/run/ind7.lean
@@ -1,7 +1,7 @@
 namespace list
   inductive list (A : Type) : Type :=
-  nil  : list A,
-  cons : A → list A → list A
+  | nil  : list A
+  | cons : A → list A → list A
 
   check list.{1}
   check list.cons.{1}
diff --git a/tests/lean/run/ind_ns.lean b/tests/lean/run/ind_ns.lean
index d1aa1734f..582ee14a5 100644
--- a/tests/lean/run/ind_ns.lean
+++ b/tests/lean/run/ind_ns.lean
@@ -1,5 +1,5 @@
 inductive day :=
-monday, tuesday, wednesday, thursday, friday, saturday, sunday
+monday | tuesday | wednesday | thursday | friday | saturday | sunday
 
 check day.monday
 open day
diff --git a/tests/lean/run/indimp.lean b/tests/lean/run/indimp.lean
index 652ed04ae..f921fc013 100644
--- a/tests/lean/run/indimp.lean
+++ b/tests/lean/run/indimp.lean
@@ -2,16 +2,16 @@ prelude
 definition Prop := Type.{0}
 
 inductive nat :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 inductive list (A : Type) :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 
 inductive list2 (A : Type) : Type :=
-nil2 {} : list2 A,
-cons2   : A → list2 A → list2 A
+| nil2 {} : list2 A
+| cons2   : A → list2 A → list2 A
 
 inductive and (A B : Prop) : Prop :=
 and_intro : A → B → and A B
diff --git a/tests/lean/run/induniv.lean b/tests/lean/run/induniv.lean
index e8b9745d4..3ab18d645 100644
--- a/tests/lean/run/induniv.lean
+++ b/tests/lean/run/induniv.lean
@@ -1,23 +1,23 @@
 prelude
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 
 section
   variable A : Type
   inductive list2 : Type :=
-  nil2 {} : list2,
-  cons2   : A → list2 → list2
+  | nil2 {} : list2
+  | cons2   : A → list2 → list2
 end
 
 constant num : Type.{1}
 
 namespace Tree
 inductive tree (A : Type) : Type :=
-node : A → forest A → tree A
+| node : A → forest A → tree A
 with forest : Type :=
-nil  : forest A,
-cons : tree A → forest A → forest A
+| nil  : forest A
+| cons : tree A → forest A → forest A
 end Tree
 
 inductive group_struct (A : Type) : Type :=
diff --git a/tests/lean/run/inf_tree.lean b/tests/lean/run/inf_tree.lean
index 8cc310f55..b53a73136 100644
--- a/tests/lean/run/inf_tree.lean
+++ b/tests/lean/run/inf_tree.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic
 open nat
 
 inductive inftree (A : Type) :=
-leaf : A → inftree A,
-node : (nat → inftree A) → inftree A
+| leaf : A → inftree A
+| node : (nat → inftree A) → inftree A
 
 namespace inftree
   inductive dsub {A : Type} : inftree A → inftree A → Prop :=
diff --git a/tests/lean/run/inf_tree2.lean b/tests/lean/run/inf_tree2.lean
index dab0f1f0f..95019e0a9 100644
--- a/tests/lean/run/inf_tree2.lean
+++ b/tests/lean/run/inf_tree2.lean
@@ -2,13 +2,13 @@ import logic data.nat.basic
 open nat
 
 inductive inftree (A : Type) : Type :=
-leaf : A → inftree A,
-node : (nat → inftree A) → inftree A → inftree A
+| leaf : A → inftree A
+| node : (nat → inftree A) → inftree A → inftree A
 
 namespace inftree
   inductive dsub {A : Type} : inftree A → inftree A → Prop :=
-  intro₁ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub (f a) (node f t),
-  intro₂ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub t (node f t)
+  | intro₁ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub (f a) (node f t)
+  | intro₂ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub t (node f t)
 
   definition dsub.node.acc {A : Type} (f : nat → inftree A) (hf : ∀a, acc dsub (f a))
                                       (t : inftree A) (ht : acc dsub t) : acc dsub (node f t) :=
diff --git a/tests/lean/run/inf_tree3.lean b/tests/lean/run/inf_tree3.lean
index d608c73b7..c6eebb6e1 100644
--- a/tests/lean/run/inf_tree3.lean
+++ b/tests/lean/run/inf_tree3.lean
@@ -2,13 +2,13 @@ import logic data.nat.basic
 open nat
 
 inductive inftree (A : Type) : Type :=
-leaf : A → inftree A,
-node : (nat → inftree A) → inftree A → inftree A
+| leaf : A → inftree A
+| node : (nat → inftree A) → inftree A → inftree A
 
 namespace inftree
   inductive dsub {A : Type} : inftree A → inftree A → Prop :=
-  intro₁ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub (f a) (node f t),
-  intro₂ : Π (f : nat → inftree A) (t : inftree A), dsub t (node f t)
+  | intro₁ : Π (f : nat → inftree A) (a : nat) (t : inftree A), dsub (f a) (node f t)
+  | intro₂ : Π (f : nat → inftree A) (t : inftree A), dsub t (node f t)
 
   definition dsub.node.acc {A : Type} (f : nat → inftree A) (hf : ∀a, acc dsub (f a))
                                       (t : inftree A) (ht : acc dsub t) : acc dsub (node f t) :=
diff --git a/tests/lean/run/inv_bug.lean b/tests/lean/run/inv_bug.lean
index 9ddd36931..905b63674 100644
--- a/tests/lean/run/inv_bug.lean
+++ b/tests/lean/run/inv_bug.lean
@@ -2,10 +2,10 @@ open nat
 open eq.ops
 
 inductive even : nat → Prop :=
-even_zero        : even zero,
-even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
+| even_zero        : even zero
+| even_succ_of_odd : ∀ {a}, odd a  → even (succ a)
 with odd : nat → Prop :=
-odd_succ_of_even : ∀ {a}, even a → odd (succ a)
+| odd_succ_of_even : ∀ {a}, even a → odd (succ a)
 
 example : even 1 → false :=
 begin
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index 75925f30d..3e049c2cb 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -2,8 +2,8 @@ import logic
 open tactic
 
 inductive list (A : Type) : Type :=
-nil {} : list A,
-cons   : A → list A → list A
+| nil {} : list A
+| cons   : A → list A → list A
 namespace list end list open list
 open eq
 
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index 527df7699..f38391905 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -12,8 +12,8 @@
 import data.nat
 open nat eq.ops
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons : T → list T → list T
+| nil {} : list T
+| cons : T → list T → list T
 
 namespace list
 theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil)
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 16cfd6a95..1a6f15a5c 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -3,8 +3,8 @@ open decidable
 open eq
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 definition refl := @eq.refl
 namespace nat
 
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index ee29522d7..dc37a99b0 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -2,8 +2,8 @@ import logic
 open eq.ops
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition plus (x y : nat) : nat
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index d6da95388..7c6dcb50a 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -2,8 +2,8 @@ import logic
 open eq.ops
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition plus (x y : nat) : nat
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index 5aca421c3..db3c094f3 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -2,8 +2,8 @@ import logic
 open eq.ops
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
 infixl `+` := add
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index d40536216..5b76a52e4 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -2,8 +2,8 @@ import logic
 open eq.ops eq
 namespace foo
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 261dffd87..85d889fe9 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -2,8 +2,8 @@ import logic
 open eq.ops
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean
index b59f7297a..db979c095 100644
--- a/tests/lean/run/nat_bug7.lean
+++ b/tests/lean/run/nat_bug7.lean
@@ -1,8 +1,8 @@
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y
diff --git a/tests/lean/run/nested_begin.lean b/tests/lean/run/nested_begin.lean
index 7765f7ef8..44533be5d 100644
--- a/tests/lean/run/nested_begin.lean
+++ b/tests/lean/run/nested_begin.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
-vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil  : vector A zero
+| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   definition no_confusion2 {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → vector.no_confusion_type P v₁ v₂ :=
diff --git a/tests/lean/run/no_confusion_bug.lean b/tests/lean/run/no_confusion_bug.lean
index 64b078a6b..a451524da 100644
--- a/tests/lean/run/no_confusion_bug.lean
+++ b/tests/lean/run/no_confusion_bug.lean
@@ -2,13 +2,13 @@ import data.nat.basic
 open nat
 
 inductive fin : nat → Type :=
-fz : Π {n : nat},         fin (succ n),
-fs : Π {n : nat}, fin n → fin (succ n)
+| fz : Π {n : nat},         fin (succ n)
+| fs : Π {n : nat}, fin n → fin (succ n)
 
 namespace fin
 
   inductive le : ∀ {n : nat}, fin n → fin n → Prop :=
-  lez : ∀ {n : nat} (j : fin (succ n)),     le fz j,
-  les : ∀ {n : nat} {i j : fin n}, le i j → le (fs i) (fs j)
+  | lez : ∀ {n : nat} (j : fin (succ n)),     le fz j
+  | les : ∀ {n : nat} {i j : fin n}, le i j → le (fs i) (fs j)
 
 end fin
diff --git a/tests/lean/run/one2.lean b/tests/lean/run/one2.lean
index e7af7ca78..340c5985f 100644
--- a/tests/lean/run/one2.lean
+++ b/tests/lean/run/one2.lean
@@ -7,8 +7,8 @@ inductive pone : Type.{0} :=
 unit : pone
 
 inductive two.{l} : Type.{max 1 l} :=
-o : two,
-u : two
+| o : two
+| u : two
 
 inductive wrap.{l} : Type.{max 1 l} :=
 mk : true → wrap
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
index e94ac433d..12df20a29 100644
--- a/tests/lean/run/opaque_hint_bug.lean
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -1,6 +1,6 @@
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons : T → list T → list T
+| nil {} : list T
+| cons : T → list T → list T
 
 
 section
diff --git a/tests/lean/run/record1.lean b/tests/lean/run/record1.lean
index d350c4107..e8d60eedd 100644
--- a/tests/lean/run/record1.lean
+++ b/tests/lean/run/record1.lean
@@ -14,7 +14,7 @@ check point.induction_on
 check point.destruct
 
 inductive color :=
-red, green, blue
+red | green | blue
 
 structure color_point (A : Type) (B : Type) extends point A B :=
 mk :: (c : color)
diff --git a/tests/lean/run/record3.lean b/tests/lean/run/record3.lean
index a413feadf..2ffb31875 100644
--- a/tests/lean/run/record3.lean
+++ b/tests/lean/run/record3.lean
@@ -5,7 +5,7 @@ structure point (A : Type) (B : Type) :=
 mk :: (x : A) (y : B)
 
 inductive color :=
-red, green, blue
+red | green | blue
 
 structure color_point (A : Type) (B : Type) extends point A B :=
 mk :: (c : color)
diff --git a/tests/lean/run/record4.lean b/tests/lean/run/record4.lean
index fa54941df..93b5f2f60 100644
--- a/tests/lean/run/record4.lean
+++ b/tests/lean/run/record4.lean
@@ -11,7 +11,7 @@ example (p : point num num) : point.mk (point.x p) (point.y p) = p :=
 point.eta p
 
 inductive color :=
-red, green, blue
+red | green | blue
 
 structure color_point (A : Type) (B : Type) extends point A B :=
 mk :: (c : color)
diff --git a/tests/lean/run/secnot.lean b/tests/lean/run/secnot.lean
index e3553de74..5a7e276f8 100644
--- a/tests/lean/run/secnot.lean
+++ b/tests/lean/run/secnot.lean
@@ -9,8 +9,8 @@ check a ◀ b
 end
 
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons   : T → list T → list T
+| nil {} : list T
+| cons   : T → list T → list T
 
 namespace list
 section
diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean
index 94b391378..fb2acec86 100644
--- a/tests/lean/run/structure_test.lean
+++ b/tests/lean/run/structure_test.lean
@@ -4,7 +4,7 @@ inductive point (A B : Type) :=
 mk : Π (x : A) (y : B), point A B
 
 inductive color [class] :=
-red, green, blue
+red | green | blue
 
 constant foo.{l} (A : Type.{l}) [H : decidable_eq A] : Type.{l}
 
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index a4735900c..d45f3e5d8 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -6,8 +6,8 @@ open inhabited decidable
 namespace play
 -- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
-inl : A → sum A B,
-inr : B → sum A B
+| inl : A → sum A B
+| inr : B → sum A B
 
 namespace sum
 reserve infixr `+`:25
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 944566d9f..6573e206c 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -1,8 +1,8 @@
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 definition add (a b : nat) : nat
diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean
index 3530578b5..c6aeca601 100644
--- a/tests/lean/run/tactic26.lean
+++ b/tests/lean/run/tactic26.lean
@@ -3,8 +3,8 @@ open tactic inhabited
 
 namespace foo
 inductive sum (A : Type) (B : Type) : Type :=
-inl  : A → sum A B,
-inr  : B → sum A B
+| inl  : A → sum A B
+| inr  : B → sum A B
 
 theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B)
 := inhabited.destruct H (λ a, inhabited.mk (sum.inl B a))
diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean
index 5c70900a5..31663a239 100644
--- a/tests/lean/run/tactic28.lean
+++ b/tests/lean/run/tactic28.lean
@@ -3,8 +3,8 @@ open tactic inhabited
 
 namespace foo
 inductive sum (A : Type) (B : Type) : Type :=
-inl  : A → sum A B,
-inr  : B → sum A B
+| inl  : A → sum A B
+| inr  : B → sum A B
 
 theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B)
 := inhabited.destruct H (λ a, inhabited.mk (sum.inl B a))
diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean
index f635168aa..7a488a79a 100644
--- a/tests/lean/run/tree.lean
+++ b/tests/lean/run/tree.lean
@@ -2,8 +2,8 @@ import logic data.prod
 open eq.ops prod
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree A → tree A → tree A
+| leaf : A → tree A
+| node : tree A → tree A → tree A
 
 inductive one.{l} : Type.{max 1 l} :=
 star : one
diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean
index 15da3feb0..2d641efb0 100644
--- a/tests/lean/run/tree2.lean
+++ b/tests/lean/run/tree2.lean
@@ -2,8 +2,8 @@ import logic data.prod
 open eq.ops prod tactic
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree A → tree A → tree A
+| leaf : A → tree A
+| node : tree A → tree A → tree A
 
 inductive one.{l} : Type.{max 1 l} :=
 star : one
diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean
index b2a3028f1..cc2f84bcc 100644
--- a/tests/lean/run/tree3.lean
+++ b/tests/lean/run/tree3.lean
@@ -2,8 +2,8 @@ import logic data.prod
 open eq.ops prod tactic
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree A → tree A → tree A
+| leaf : A → tree A
+| node : tree A → tree A → tree A
 
 inductive one.{l} : Type.{max 1 l} :=
 star : one
diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean
index bb66b851c..74bc68593 100644
--- a/tests/lean/run/tree_height.lean
+++ b/tests/lean/run/tree_height.lean
@@ -2,8 +2,8 @@ import logic data.nat
 open eq.ops nat
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree A → tree A → tree A
+| leaf : A → tree A
+| node : tree A → tree A → tree A
 
 namespace tree
 
diff --git a/tests/lean/run/tree_subterm_pred.lean b/tests/lean/run/tree_subterm_pred.lean
index 51c32891f..7b4c2cb58 100644
--- a/tests/lean/run/tree_subterm_pred.lean
+++ b/tests/lean/run/tree_subterm_pred.lean
@@ -2,14 +2,14 @@ import logic
 open eq.ops
 
 inductive tree (A : Type) :=
-leaf : A → tree A,
-node : tree A → tree A → tree A
+| leaf : A → tree A
+| node : tree A → tree A → tree A
 
 namespace tree
 
 inductive direct_subterm {A : Type} : tree A → tree A → Prop :=
-node_l : Π (l r : tree A), direct_subterm l (node l r),
-node_r : Π (l r : tree A), direct_subterm r (node l r)
+| node_l : Π (l r : tree A), direct_subterm l (node l r)
+| node_r : Π (l r : tree A), direct_subterm r (node l r)
 
 definition direct_subterm.wf {A : Type} : well_founded (@direct_subterm A) :=
 well_founded.intro (λ t : tree A,
diff --git a/tests/lean/run/uni.lean b/tests/lean/run/uni.lean
index 1011cf462..311e866eb 100644
--- a/tests/lean/run/uni.lean
+++ b/tests/lean/run/uni.lean
@@ -1,8 +1,8 @@
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 check @nat.rec
 
diff --git a/tests/lean/run/uni2.lean b/tests/lean/run/uni2.lean
index 625e03a50..86d61f014 100644
--- a/tests/lean/run/uni2.lean
+++ b/tests/lean/run/uni2.lean
@@ -1,8 +1,8 @@
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 constant f : nat → nat
 
diff --git a/tests/lean/run/uni_issue1.lean b/tests/lean/run/uni_issue1.lean
index 8aceff03d..992289dba 100644
--- a/tests/lean/run/uni_issue1.lean
+++ b/tests/lean/run/uni_issue1.lean
@@ -1,8 +1,8 @@
 import logic
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 definition is_zero (n : nat)
 := nat.rec true (λ n r, false) n
diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean
index b5eae2982..5fa87dfe2 100644
--- a/tests/lean/run/univ_problem.lean
+++ b/tests/lean/run/univ_problem.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic data.prod data.unit
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
-vnil {} : vector A zero,
-vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil {} : vector A zero
+| vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   print definition vector.no_confusion
diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean
index ccff603e3..1ef3c6d4c 100644
--- a/tests/lean/run/uuu.lean
+++ b/tests/lean/run/uuu.lean
@@ -8,16 +8,16 @@ inductive unit : Type :=
 tt : unit
 definition tt := @unit.tt
 inductive nat : Type :=
-O : nat,
-S : nat → nat
+| O : nat
+| S : nat → nat
 
 inductive paths {A : Type} (a : A) : A → Type :=
 idpath : paths a a
 definition idpath := @paths.idpath
 
 inductive sum (A : Type) (B : Type) : Type :=
-inl : A -> sum A B,
-inr : B -> sum A B
+| inl : A -> sum A B
+| inr : B -> sum A B
 
 definition coprod := sum
 definition ii1fun {A : Type} (B : Type) (a : A) := sum.inl B a
diff --git a/tests/lean/run/vars_anywhere.lean b/tests/lean/run/vars_anywhere.lean
index fd48344ae..b7dd0179b 100644
--- a/tests/lean/run/vars_anywhere.lean
+++ b/tests/lean/run/vars_anywhere.lean
@@ -5,7 +5,7 @@ definition id (a : A) := a
 check @id
 
 inductive list :=
-nil : list,
-cons : A → list → list
+| nil : list
+| cons : A → list → list
 
 check @list.cons
diff --git a/tests/lean/run/vec_inv.lean b/tests/lean/run/vec_inv.lean
index 681d64eb1..053de401c 100644
--- a/tests/lean/run/vec_inv.lean
+++ b/tests/lean/run/vec_inv.lean
@@ -2,8 +2,8 @@ import data.nat.basic data.empty data.prod
 open nat eq.ops prod
 
 inductive vector (T : Type) : ℕ → Type :=
-  nil {} : vector T 0,
-  cons : T → ∀{n}, vector T n → vector T (succ n)
+| nil {} : vector T 0
+| cons : T → ∀{n}, vector T n → vector T (succ n)
 
 set_option pp.metavar_args true
 set_option pp.implicit true
diff --git a/tests/lean/run/vec_inv2.lean b/tests/lean/run/vec_inv2.lean
index 18c42f35c..be5cacfb8 100644
--- a/tests/lean/run/vec_inv2.lean
+++ b/tests/lean/run/vec_inv2.lean
@@ -2,8 +2,8 @@ import data.nat.basic data.empty data.prod
 open nat eq.ops prod
 
 inductive vector (T : Type) : ℕ → Type :=
-  nil {} : vector T 0,
-  cons : T → ∀{n}, vector T n → vector T (succ n)
+|  nil {} : vector T 0
+|  cons : T → ∀{n}, vector T n → vector T (succ n)
 
 set_option pp.metavar_args true
 set_option pp.implicit true
diff --git a/tests/lean/run/vec_inv3.lean b/tests/lean/run/vec_inv3.lean
index a6e927979..e92290a16 100644
--- a/tests/lean/run/vec_inv3.lean
+++ b/tests/lean/run/vec_inv3.lean
@@ -2,8 +2,8 @@ import data.nat.basic data.empty data.prod
 open nat eq.ops prod
 
 inductive vector (T : Type) : ℕ → Type :=
-  nil {} : vector T 0,
-  cons : T → ∀{n}, vector T n → vector T (succ n)
+| nil {} : vector T 0
+| cons : T → ∀{n}, vector T n → vector T (succ n)
 
 set_option pp.metavar_args true
 set_option pp.implicit true
diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index a1ee3a93c..ad84cbfe9 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic data.prod data.unit
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
-vnil {} : vector A zero,
-vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil {} : vector A zero
+| vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   -- print definition no_confusion
diff --git a/tests/lean/run/vector2.lean b/tests/lean/run/vector2.lean
index 32a9b49e4..f1d868565 100644
--- a/tests/lean/run/vector2.lean
+++ b/tests/lean/run/vector2.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
-vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil  : vector A zero
+| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
diff --git a/tests/lean/run/vector3.lean b/tests/lean/run/vector3.lean
index 6ffa45c6c..81b299921 100644
--- a/tests/lean/run/vector3.lean
+++ b/tests/lean/run/vector3.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic
 open nat
 
 inductive vector (A : Type) : nat → Type :=
-vnil  : vector A zero,
-vcons : Π {n : nat}, A → vector A n → vector A (succ n)
+| vnil  : vector A zero
+| vcons : Π {n : nat}, A → vector A n → vector A (succ n)
 
 namespace vector
   theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ :=
diff --git a/tests/lean/run/vector_subterm_pred.lean b/tests/lean/run/vector_subterm_pred.lean
index 1cca841ac..85c305118 100644
--- a/tests/lean/run/vector_subterm_pred.lean
+++ b/tests/lean/run/vector_subterm_pred.lean
@@ -2,8 +2,8 @@ import logic data.nat.basic data.sigma
 open nat eq.ops sigma
 
 inductive vector (A : Type) : nat → Type :=
-nil  : vector A zero,
-cons : A → (Π{n}, vector A n → vector A (succ n))
+| nil  : vector A zero
+| cons : A → (Π{n}, vector A n → vector A (succ n))
 
 namespace vector
 
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 632e862b6..b06f9817e 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -17,8 +17,8 @@ open nat
 open eq.ops eq
 
 inductive list (T : Type) : Type :=
-nil {} : list T,
-cons : T → list T → list T
+| nil {} : list T
+| cons : T → list T → list T
 
 definition refl := @eq.refl
 
diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean
index 2527de427..6632f2754 100644
--- a/tests/lean/slow/nat_bug1.lean
+++ b/tests/lean/slow/nat_bug1.lean
@@ -8,8 +8,8 @@ open tactic
 
 namespace foo
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 notation `ℕ`:max := nat
 
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index f12bbcc76..dee720fc5 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -13,8 +13,8 @@ definition or_intro_left := @or.intro_left
 definition or_intro_right := @or.intro_right
 
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 namespace nat
 
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 4f75a184c..1ea1782e6 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -9,8 +9,8 @@ open decidable
 
 namespace experiment
 inductive nat : Type :=
-zero : nat,
-succ : nat → nat
+| zero : nat
+| succ : nat → nat
 
 
 namespace nat