From 5ca52d81ec2f094b6402e1826ed09764b01969f0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Feb 2015 16:20:44 -0800
Subject: [PATCH] feat(frontends/lean): ML-like notation for match and
 recursive equations

---
 hott/types/sigma.hlean                 |  20 ++--
 library/data/fin.lean                  |  68 ++++++------
 library/data/int/div.lean              |   4 +-
 library/data/list/basic.lean           | 138 ++++++++++++-------------
 library/data/subtype.lean              |   2 +-
 library/data/sum.lean                  |  20 ++--
 library/data/vector.lean               |  94 ++++++++---------
 library/init/nat.lean                  |  16 +--
 library/init/tactic.lean               |   2 +-
 src/frontends/lean/decl_cmds.cpp       |  28 +++--
 tests/lean/bad_eqns.lean               |  38 +++----
 tests/lean/bad_eqns.lean.expected.out  |   4 +-
 tests/lean/hott/def_bug1.hlean         |  12 +--
 tests/lean/hott/eq1.hlean              |   4 +-
 tests/lean/nonexhaustive.lean          |  12 +--
 tests/lean/place_eqn.lean              |   6 +-
 tests/lean/place_eqn.lean.expected.out |   4 +-
 tests/lean/run/assert_tac2.lean        |   6 +-
 tests/lean/run/eq1.lean                |  16 +--
 tests/lean/run/eq10.lean               |  14 +--
 tests/lean/run/eq11.lean               |  12 +--
 tests/lean/run/eq12.lean               |  10 +-
 tests/lean/run/eq13.lean               |  14 +--
 tests/lean/run/eq14.lean               |  16 +--
 tests/lean/run/eq15.lean               |   6 +-
 tests/lean/run/eq16.lean               |   6 +-
 tests/lean/run/eq17.lean               |   6 +-
 tests/lean/run/eq18.lean               |   6 +-
 tests/lean/run/eq19.lean               |   6 +-
 tests/lean/run/eq2.lean                |   8 +-
 tests/lean/run/eq20.lean               |   6 +-
 tests/lean/run/eq21.lean               |   6 +-
 tests/lean/run/eq22.lean               |   6 +-
 tests/lean/run/eq23.lean               |   6 +-
 tests/lean/run/eq24.lean               |  24 ++---
 tests/lean/run/eq25.lean               |   6 +-
 tests/lean/run/eq3.lean                |   4 +-
 tests/lean/run/eq4.lean                |   8 +-
 tests/lean/run/eq5.lean                |   8 +-
 tests/lean/run/eq6.lean                |   6 +-
 tests/lean/run/eq7.lean                |   6 +-
 tests/lean/run/eq8.lean                |   6 +-
 tests/lean/run/eq9.lean                |  12 +--
 tests/lean/run/eqn_tac.lean            |  12 +--
 tests/lean/run/finbug.lean             |  24 ++---
 tests/lean/run/finbug2.lean            |  24 ++---
 tests/lean/run/match3.lean             |  34 +++---
 tests/lean/run/match4.lean             |   8 +-
 tests/lean/run/sigma_match.lean        |   4 +-
 tests/lean/run/unzip_bug.lean          |   6 +-
 tests/lean/shadow.lean                 |   6 +-
 tests/lean/shadow.lean.expected.out    |   2 +-
 tests/lean/unzip_error.lean            |   6 +-
 53 files changed, 420 insertions(+), 408 deletions(-)

diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index f7a78888b..374300482 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -17,14 +17,14 @@ namespace sigma
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
   -- sigma.eta is already used for the eta rule for strict equality
-  protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u,
-  eta ⟨u₁, u₂⟩ := idp
+  protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u
+  | eta ⟨u₁, u₂⟩ := idp
 
-  definition eta2 : Π (u : Σa b, C a b), ⟨u.1, u.2.1, u.2.2⟩ = u,
-  eta2 ⟨u₁, u₂, u₃⟩ := idp
+  definition eta2 : Π (u : Σa b, C a b), ⟨u.1, u.2.1, u.2.2⟩ = u
+  | eta2 ⟨u₁, u₂, u₃⟩ := idp
 
-  definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u,
-  eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
+  definition eta3 : Π (u : Σa b c, D a b c), ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u
+  | eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp
 
   definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : ⟨a, b⟩ = ⟨a', b'⟩ :=
   by cases p; cases q; apply idp
@@ -68,12 +68,12 @@ namespace sigma
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_eq_uncurried : Π (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v), u = v,
-  sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
+  definition sigma_eq_uncurried : Π (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v), u = v
+  | sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
 
   definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2),
-        sigma.mk (sigma_eq_uncurried pq)..1 (sigma_eq_uncurried pq)..2 = pq,
-  dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
+        sigma.mk (sigma_eq_uncurried pq)..1 (sigma_eq_uncurried pq)..2 = pq
+  | dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
 
   definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
       : (sigma_eq_uncurried pq)..1 = pq.1 :=
diff --git a/library/data/fin.lean b/library/data/fin.lean
index 05b9b039e..fea0d20aa 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -15,9 +15,9 @@ fz : Π n, fin (succ n),
 fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
-  definition to_nat : Π {n}, fin n → nat,
-  @to_nat ⌞n+1⌟ (fz n) := zero,
-  @to_nat ⌞n+1⌟ (fs f) := succ (to_nat f)
+  definition to_nat : Π {n}, fin n → nat
+  | @to_nat ⌞n+1⌟ (fz n) := zero
+  | @to_nat ⌞n+1⌟ (fs f) := succ (to_nat f)
 
   theorem to_nat_fz (n : nat) : to_nat (fz n) = zero :=
   rfl
@@ -25,17 +25,17 @@ namespace fin
   theorem to_nat_fs {n : nat} (f : fin n) : to_nat (fs f) = succ (to_nat f) :=
   rfl
 
-  theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n,
-  to_nat_lt (fz n) :=  calc
-    to_nat (fz n) = 0    : rfl
-             ...  < n+1  : succ_pos n,
-  to_nat_lt (@fs n f) := calc
-     to_nat (fs f) = (to_nat f)+1 : rfl
-              ...  < n+1          : succ_lt_succ (to_nat_lt f)
+  theorem to_nat_lt : Π {n} (f : fin n), to_nat f < n
+  | to_nat_lt (fz n) :=  calc
+      to_nat (fz n) = 0    : rfl
+               ...  < n+1  : succ_pos n
+  | to_nat_lt (@fs n f) := calc
+      to_nat (fs f) = (to_nat f)+1 : rfl
+               ...  < n+1          : succ_lt_succ (to_nat_lt f)
 
-  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n),
-  @lift ⌞n+1⌟ (fz n)     m := fz (m + n),
-  @lift ⌞n+1⌟ (@fs n f)  m := fs (lift f m)
+  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (m + n)
+  | @lift ⌞n+1⌟ (fz n)     m := fz (m + n)
+  | @lift ⌞n+1⌟ (@fs n f)  m := fs (lift f m)
 
   theorem lift_fz (n m : nat) : lift (fz n) m = fz (m + n) :=
   rfl
@@ -43,18 +43,18 @@ namespace fin
   theorem lift_fs {n : nat} (f : fin n) (m : nat) : lift (fs f) m = fs (lift f m) :=
   rfl
 
-  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
-  to_nat_lift (fz n) m    := rfl,
-  to_nat_lift (@fs n f) m := calc
+  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
+  | to_nat_lift (fz n) m    := rfl
+  | to_nat_lift (@fs n f) m := calc
       to_nat (fs f) = (to_nat f) + 1           : rfl
                ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
                ...  = to_nat (lift (fs f) m)   : rfl
 
-  definition of_nat : Π (p : nat) (n : nat), p < n → fin n,
-  of_nat 0     0     h := absurd h (not_lt_zero zero),
-  of_nat 0     (n+1) h := fz n,
-  of_nat (p+1) 0     h := absurd h (not_lt_zero (succ p)),
-  of_nat (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
+  definition of_nat : Π (p : nat) (n : nat), p < n → fin n
+  | of_nat 0     0     h := absurd h (not_lt_zero zero)
+  | of_nat 0     (n+1) h := fz n
+  | of_nat (p+1) 0     h := absurd h (not_lt_zero (succ p))
+  | of_nat (p+1) (n+1) h := fs (of_nat p n (lt_of_succ_lt_succ h))
 
   theorem of_nat_zero_succ (n : nat) (h : 0 < n+1) : of_nat 0 (n+1) h = fz n :=
   rfl
@@ -63,19 +63,19 @@ namespace fin
                of_nat (p+1) (n+1) h = fs (of_nat p n (lt_of_succ_lt_succ h)) :=
   rfl
 
-  theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p,
-  to_nat_of_nat 0     0     h := absurd h (not_lt_zero 0),
-  to_nat_of_nat 0     (n+1) h := rfl,
-  to_nat_of_nat (p+1) 0     h := absurd h (not_lt_zero (p+1)),
-  to_nat_of_nat (p+1) (n+1) h := calc
-    to_nat (of_nat (p+1) (n+1) h)
-             = succ (to_nat (of_nat p n _)) : rfl
-         ... = succ p                       : {to_nat_of_nat p n _}
+  theorem to_nat_of_nat : ∀ (p : nat) (n : nat) (h : p < n), to_nat (of_nat p n h) = p
+  | to_nat_of_nat 0     0     h := absurd h (not_lt_zero 0)
+  | to_nat_of_nat 0     (n+1) h := rfl
+  | to_nat_of_nat (p+1) 0     h := absurd h (not_lt_zero (p+1))
+  | to_nat_of_nat (p+1) (n+1) h := calc
+      to_nat (of_nat (p+1) (n+1) h)
+               = succ (to_nat (of_nat p n _)) : rfl
+           ... = succ p                       : {to_nat_of_nat p n _}
 
-  theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f,
-  of_nat_to_nat (fz n) h    := rfl,
-  of_nat_to_nat (@fs n f) h := calc
-    of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
-                                 ...  = fs f                       : {of_nat_to_nat f _}
+  theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f
+  | of_nat_to_nat (fz n) h    := rfl
+  | of_nat_to_nat (@fs n f) h := calc
+      of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
+                                   ...  = fs f                       : {of_nat_to_nat f _}
 
 end fin
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 9fb49809d..bf046c6eb 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -24,8 +24,8 @@ namespace int
 definition divide (a b : ℤ) : ℤ :=
 sign b *
   (match a with
-    of_nat m := #nat m div (nat_abs b),
-    -[ m +1] := -[ (#nat m div (nat_abs b)) +1]
+    | of_nat m := #nat m div (nat_abs b)
+    | -[ m +1] := -[ (#nat m div (nat_abs b)) +1]
   end)
 
 notation a div b := divide a b
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index c3cbb2fae..2d4fef642 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -24,9 +24,9 @@ variable {T : Type}
 
 /- append -/
 
-definition append : list T → list T → list T,
-append nil l      := l,
-append (h :: s) t := h :: (append s t)
+definition append : list T → list T → list T
+| append nil l      := l
+| append (h :: s) t := h :: (append s t)
 
 notation l₁ ++ l₂ := append l₁ l₂
 
@@ -34,66 +34,66 @@ theorem append_nil_left (t : list T) : nil ++ t = t
 
 theorem append_cons (x : T) (s t : list T) : (x::s) ++ t = x::(s ++ t)
 
-theorem append_nil_right : ∀ (t : list T), t ++ nil = t,
-append_nil_right nil      := rfl,
-append_nil_right (a :: l) := calc
+theorem append_nil_right : ∀ (t : list T), t ++ nil = t
+| append_nil_right nil      := rfl
+| append_nil_right (a :: l) := calc
   (a :: l) ++ nil = a :: (l ++ nil) : rfl
               ... = a :: l          : append_nil_right l
 
 
-theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u),
-append.assoc nil t u      := rfl,
-append.assoc (a :: l) t u := calc
+theorem append.assoc : ∀ (s t u : list T), s ++ t ++ u = s ++ (t ++ u)
+| append.assoc nil t u      := rfl
+| append.assoc (a :: l) t u := calc
   (a :: l) ++ t ++ u = a :: (l ++ t ++ u)   : rfl
                  ... = a :: (l ++ (t ++ u)) : append.assoc
                  ... = (a :: l) ++ (t ++ u) : rfl
 
 /- length -/
 
-definition length : list T → nat,
-length nil      := 0,
-length (a :: l) := length l + 1
+definition length : list T → nat
+| length nil      := 0
+| length (a :: l) := length l + 1
 
 theorem length_nil : length (@nil T) = 0
 
 theorem length_cons (x : T) (t : list T) : length (x::t) = length t + 1
 
-theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t,
-length_append nil t      := calc
-  length (nil ++ t)  = length t : rfl
-                 ... = length nil + length t : zero_add,
-length_append (a :: s) t := calc
-  length (a :: s ++ t) = length (s ++ t) + 1        : rfl
-                  ...  = length s + length t + 1    : length_append
-                  ...  = (length s + 1) + length t  : add.succ_left
-                  ...  = length (a :: s) + length t : rfl
+theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length t
+| length_append nil t      := calc
+    length (nil ++ t)  = length t : rfl
+                   ... = length nil + length t : zero_add
+| length_append (a :: s) t := calc
+    length (a :: s ++ t) = length (s ++ t) + 1        : rfl
+                    ...  = length s + length t + 1    : length_append
+                    ...  = (length s + 1) + length t  : add.succ_left
+                    ...  = length (a :: s) + length t : rfl
 
 -- add_rewrite length_nil length_cons
 
 /- concat -/
 
-definition concat : Π (x : T), list T → list T,
-concat a nil      := [a],
-concat a (b :: l) := b :: concat a l
+definition concat : Π (x : T), list T → list T
+| concat a nil      := [a]
+| concat a (b :: l) := b :: concat a l
 
 theorem concat_nil (x : T) : concat x nil = [x]
 
 theorem concat_cons (x y : T) (l : list T) : concat x (y::l)  = y::(concat x l)
 
-theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a],
-concat_eq_append nil      := rfl,
-concat_eq_append (b :: l) := calc
-  concat a (b :: l) = b :: (concat a l) : rfl
-               ...  = b :: (l ++ [a])   : concat_eq_append
-               ...  = (b :: l) ++ [a]   : rfl
+theorem concat_eq_append (a : T) : ∀ (l : list T), concat a l = l ++ [a]
+| concat_eq_append nil      := rfl
+| concat_eq_append (b :: l) := calc
+    concat a (b :: l) = b :: (concat a l) : rfl
+                 ...  = b :: (l ++ [a])   : concat_eq_append
+                 ...  = (b :: l) ++ [a]   : rfl
 
 -- add_rewrite append_nil append_cons
 
 /- reverse -/
 
-definition reverse : list T → list T,
-reverse nil      := nil,
-reverse (a :: l) := concat a (reverse l)
+definition reverse : list T → list T
+| reverse nil      := nil
+| reverse (a :: l) := concat a (reverse l)
 
 theorem reverse_nil : reverse (@nil T) = nil
 
@@ -101,27 +101,27 @@ theorem reverse_cons (x : T) (l : list T) : reverse (x::l) = concat x (reverse l
 
 theorem reverse_singleton (x : T) : reverse [x] = [x]
 
-theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s),
-reverse_append nil t2      := calc
-  reverse (nil ++ t2) = reverse t2                    : rfl
-               ...    = (reverse t2) ++ nil           : append_nil_right
-               ...    = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹},
-reverse_append (a2 :: s2) t2 := calc
-  reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2))         : rfl
-                      ...    = concat a2 (reverse t2 ++ reverse s2)   : reverse_append
-                      ...    = (reverse t2 ++ reverse s2) ++ [a2]     : concat_eq_append
-                      ...    = reverse t2 ++ (reverse s2 ++ [a2])     : append.assoc
-                      ...    = reverse t2 ++ concat a2 (reverse s2)   : concat_eq_append
-                      ...    = reverse t2 ++ reverse (a2 :: s2)       : rfl
+theorem reverse_append : ∀ (s t : list T), reverse (s ++ t) = (reverse t) ++ (reverse s)
+| reverse_append nil t2      := calc
+    reverse (nil ++ t2) = reverse t2                    : rfl
+                 ...    = (reverse t2) ++ nil           : append_nil_right
+                 ...    = (reverse t2) ++ (reverse nil) : {reverse_nil⁻¹}
+| reverse_append (a2 :: s2) t2 := calc
+    reverse ((a2 :: s2) ++ t2) = concat a2 (reverse (s2 ++ t2))         : rfl
+                        ...    = concat a2 (reverse t2 ++ reverse s2)   : reverse_append
+                        ...    = (reverse t2 ++ reverse s2) ++ [a2]     : concat_eq_append
+                        ...    = reverse t2 ++ (reverse s2 ++ [a2])     : append.assoc
+                        ...    = reverse t2 ++ concat a2 (reverse s2)   : concat_eq_append
+                        ...    = reverse t2 ++ reverse (a2 :: s2)       : rfl
 
-theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l,
-reverse_reverse nil      := rfl,
-reverse_reverse (a :: l) := calc
-  reverse (reverse (a :: l)) = reverse (concat a (reverse l))     : rfl
-                        ...  = reverse (reverse l ++ [a])         : concat_eq_append
-                        ...  = reverse [a] ++ reverse (reverse l) : reverse_append
-                        ...  = reverse [a] ++ l                   : reverse_reverse
-                        ...  = a :: l                             : rfl
+theorem reverse_reverse : ∀ (l : list T), reverse (reverse l) = l
+| reverse_reverse nil      := rfl
+| reverse_reverse (a :: l) := calc
+    reverse (reverse (a :: l)) = reverse (concat a (reverse l))     : rfl
+                          ...  = reverse (reverse l ++ [a])         : concat_eq_append
+                          ...  = reverse [a] ++ reverse (reverse l) : reverse_append
+                          ...  = reverse [a] ++ l                   : reverse_reverse
+                          ...  = a :: l                             : rfl
 
 theorem concat_eq_reverse_cons (x : T) (l : list T) : concat x l = reverse (x :: reverse l) :=
 calc
@@ -130,9 +130,9 @@ calc
 
 /- head and tail -/
 
-definition head [h : inhabited T] : list T → T,
-head nil      := arbitrary T,
-head (a :: l) := a
+definition head [h : inhabited T] : list T → T
+| head nil      := arbitrary T
+| head (a :: l) := a
 
 theorem head_cons [h : inhabited T] (a : T) (l : list T) : head (a::l) = a
 
@@ -145,9 +145,9 @@ list.cases_on s
                    ... = x                    : head_cons
                    ... = head (x::s)          : rfl)
 
-definition tail : list T → list T,
-tail nil      := nil,
-tail (a :: l) := l
+definition tail : list T → list T
+| tail nil      := nil
+| tail (a :: l) := l
 
 theorem tail_nil : tail (@nil T) = nil
 
@@ -160,9 +160,9 @@ list.cases_on l
 
 /- list membership -/
 
-definition mem : T → list T → Prop,
-mem a nil      := false,
-mem a (b :: l) := a = b ∨ mem a l
+definition mem : T → list T → Prop
+| mem a nil      := false
+| mem a (b :: l) := a = b ∨ mem a l
 
 notation e ∈ s := mem e s
 
@@ -246,9 +246,9 @@ section
 variable [H : decidable_eq T]
 include H
 
-definition find : T → list T → nat,
-find a nil      := 0,
-find a (b :: l) := if a = b then 0 else succ (find a l)
+definition find : T → list T → nat
+| find a nil      := 0
+| find a (b :: l) := if a = b then 0 else succ (find a l)
 
 theorem find_nil (x : T) : find x nil = 0
 
@@ -271,10 +271,10 @@ end
 
 /- nth element -/
 
-definition nth [h : inhabited T] : list T → nat → T,
-nth nil      n     := arbitrary T,
-nth (a :: l) 0     := a,
-nth (a :: l) (n+1) := nth l n
+definition nth [h : inhabited T] : list T → nat → T
+| nth nil      n     := arbitrary T
+| nth (a :: l) 0     := a
+| nth (a :: l) (n+1) := nth l n
 
 theorem nth_zero [h : inhabited T] (a : T) (l : list T) : nth (a :: l) 0 = a
 
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index 2311a4b26..314a76deb 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -13,7 +13,7 @@ set_option structure.proj_mk_thm true
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binders:55 `|` r:(scoped:1 P, subtype P) `}` := r
+notation `{` binders `|` r:(scoped:1 P, subtype P) `}` := r
 
 namespace subtype
   variables {A : Type} {P : A → Prop}
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 17488a057..7a22cbdf7 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -39,17 +39,17 @@ namespace sum
   protected definition is_inhabited_right [instance] [h : inhabited B] : inhabited (A + B) :=
   inhabited.mk (inr (default B))
 
-  protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂),
-  has_decidable_eq (inl a₁) (inl a₂) :=
+  protected definition has_decidable_eq [instance] [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ s₁ s₂ : A + B, decidable (s₁ = s₂)
+  | has_decidable_eq (inl a₁) (inl a₂) :=
     match h₁ a₁ a₂ with
-      decidable.inl hp := decidable.inl (hp ▸ rfl),
-      decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn)
-    end,
-  has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e),
-  has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e),
-  has_decidable_eq (inr b₁) (inr b₂) :=
+      | decidable.inl hp := decidable.inl (hp ▸ rfl)
+      | decidable.inr hn := decidable.inr (λ he, absurd (inl_inj he) hn)
+    end
+  | has_decidable_eq (inl a₁) (inr b₂) := decidable.inr (λ e, sum.no_confusion e)
+  | has_decidable_eq (inr b₁) (inl a₂) := decidable.inr (λ e, sum.no_confusion e)
+  | has_decidable_eq (inr b₁) (inr b₂) :=
     match h₂ b₁ b₂ with
-      decidable.inl hp := decidable.inl (hp ▸ rfl),
-      decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn)
+      | decidable.inl hp := decidable.inl (hp ▸ rfl)
+      | decidable.inr hn := decidable.inr (λ he, absurd (inr_inj he) hn)
     end
 end sum
diff --git a/library/data/vector.lean b/library/data/vector.lean
index 37249bbda..8fe141fcc 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -18,18 +18,18 @@ namespace vector
 
   variables {A B C : Type}
 
-  protected definition is_inhabited [instance] [h : inhabited A] : ∀ (n : nat), inhabited (vector A n),
-  is_inhabited 0     := inhabited.mk nil,
-  is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
+  protected definition is_inhabited [instance] [h : inhabited A] : ∀ (n : nat), inhabited (vector A n)
+  | is_inhabited 0     := inhabited.mk nil
+  | is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
 
-  theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil,
-  vector0_eq_nil nil := rfl
+  theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil
+  | vector0_eq_nil nil := rfl
 
-  definition head : Π {n : nat}, vector A (succ n) → A,
-  head (a::v) := a
+  definition head : Π {n : nat}, vector A (succ n) → A
+  | head (a::v) := a
 
-  definition tail : Π {n : nat}, vector A (succ n) → vector A n,
-  tail (a::v) := v
+  definition tail : Π {n : nat}, vector A (succ n) → vector A n
+  | tail (a::v) := v
 
   theorem head_cons {n : nat} (h : A) (t : vector A n) : head (h :: t) = h :=
   rfl
@@ -37,12 +37,12 @@ namespace vector
   theorem tail_cons {n : nat} (h : A) (t : vector A n) : tail (h :: t) = t :=
   rfl
 
-  theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v,
-  eta (a::v) := rfl
+  theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v
+  | eta (a::v) := rfl
 
-  definition last : Π {n : nat}, vector A (succ n) → A,
-  last (a::nil) := a,
-  last (a::v)   := last v
+  definition last : Π {n : nat}, vector A (succ n) → A
+  | last (a::nil) := a
+  | last (a::v)   := last v
 
   theorem last_singleton (a : A) : last (a :: nil) = a :=
   rfl
@@ -50,20 +50,20 @@ namespace vector
   theorem last_cons {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
   rfl
 
-  definition const : Π (n : nat), A → vector A n,
-  const 0        a := nil,
-  const (succ n) a := a :: const n a
+  definition const : Π (n : nat), A → vector A n
+  | const 0        a := nil
+  | const (succ n) a := a :: const n a
 
   theorem head_const (n : nat) (a : A) : head (const (succ n) a) = a :=
   rfl
 
-  theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a,
-  last_const 0        a := rfl,
-  last_const (succ n) a := last_const n a
+  theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a
+  | last_const 0        a := rfl
+  | last_const (succ n) a := last_const n a
 
-  definition map (f : A → B) : Π {n : nat}, vector A n → vector B n,
-  map nil    := nil,
-  map (a::v) := f a :: map v
+  definition map (f : A → B) : Π {n : nat}, vector A n → vector B n
+  | map nil    := nil
+  | map (a::v) := f a :: map v
 
   theorem map_nil (f : A → B) : map f nil = nil :=
   rfl
@@ -71,9 +71,9 @@ namespace vector
   theorem map_cons {n : nat} (f : A → B) (h : A) (t : vector A n) : map f (h :: t) =  f h :: map f t :=
   rfl
 
-  definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n,
-  map2 nil     nil     := nil,
-  map2 (a::va) (b::vb) := f a b :: map2 va vb
+  definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
+  | map2 nil     nil     := nil
+  | map2 (a::va) (b::vb) := f a b :: map2 va vb
 
   theorem map2_nil (f : A → B → C) : map2 f nil nil = nil :=
   rfl
@@ -83,9 +83,9 @@ namespace vector
   rfl
 
   -- Remark: why do we need to provide indices?
-  definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m),
-  @append 0        m nil    w := w,
-  @append (succ n) m (a::v) w := a :: (append v w)
+  definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m)
+  | @append 0        m nil    w := w
+  | @append (succ n) m (a::v) w := a :: (append v w)
 
   theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
   rfl
@@ -94,9 +94,9 @@ namespace vector
     append (h::t) v = h :: (append t v) :=
   rfl
 
-  definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
-  unzip nil           := (nil, nil),
-  unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
+  definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
+  | unzip nil           := (nil, nil)
+  | unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
 
   theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil) :=
   rfl
@@ -105,9 +105,9 @@ namespace vector
        unzip ((a, b) :: v) = (a :: pr₁ (unzip v), b :: pr₂ (unzip v)) :=
   rfl
 
-  definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n,
-  zip nil     nil     := nil,
-  zip (a::va) (b::vb) := ((a, b) :: zip va vb)
+  definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n
+  | zip nil     nil     := nil
+  | zip (a::va) (b::vb) := ((a, b) :: zip va vb)
 
   theorem zip_nil_nil : zip (@nil A) (@nil B) = nil :=
   rfl
@@ -116,26 +116,26 @@ namespace vector
       zip (a::va) (b::vb) = ((a, b) :: zip va vb) :=
   rfl
 
-  theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂),
-  @unzip_zip 0        nil     nil     := rfl,
-  @unzip_zip (succ n) (a::va) (b::vb) := calc
+  theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂)
+  | @unzip_zip 0        nil     nil     := rfl
+  | @unzip_zip (succ n) (a::va) (b::vb) := calc
        unzip (zip (a :: va) (b :: vb))
              = (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl
         ...  = (a :: pr₁ (va, vb), b :: pr₂ (va, vb))                       : {unzip_zip va vb}
         ...  = (a :: va, b :: vb)                                           : rfl
 
-  theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v,
-  @zip_unzip 0        nil            := rfl,
-  @zip_unzip (succ n) ((a, b) :: v)  := calc
+  theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
+  | @zip_unzip 0        nil            := rfl
+  | @zip_unzip (succ n) ((a, b) :: v)  := calc
     zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
          = (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
      ... = (a, b) :: v                                   : {zip_unzip v}
 
   /- Concat -/
 
-  definition concat : Π {n : nat}, vector A n → A → vector A (succ n),
-  concat nil    a := a :: nil,
-  concat (b::v) a := b :: concat v a
+  definition concat : Π {n : nat}, vector A n → A → vector A (succ n)
+  | concat nil    a := a :: nil
+  | concat (b::v) a := b :: concat v a
 
   theorem concat_nil (a : A) : concat nil a = a :: nil :=
   rfl
@@ -143,9 +143,9 @@ namespace vector
   theorem concat_cons {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
   rfl
 
-  theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a,
-  @last_concat 0        nil    a := rfl,
-  @last_concat (succ n) (b::v) a := calc
+  theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a
+  | @last_concat 0        nil    a := rfl
+  | @last_concat (succ n) (b::v) a := calc
     last (concat (b::v) a) = last (concat v a) : rfl
                     ...    = a                 : last_concat v a
 end vector
diff --git a/library/init/nat.lean b/library/init/nat.lean
index e6a5ef852..62c3a78dc 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -29,14 +29,14 @@ namespace nat
   protected definition is_inhabited [instance] : inhabited nat :=
   inhabited.mk zero
 
-  protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y),
-  has_decidable_eq zero     zero     := inl rfl,
-  has_decidable_eq (succ x) zero     := inr (λ h, nat.no_confusion h),
-  has_decidable_eq zero     (succ y) := inr (λ h, nat.no_confusion h),
-  has_decidable_eq (succ x) (succ y) :=
-    if H : x = y
-    then inl (eq.rec_on H rfl)
-    else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
+  protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
+  | has_decidable_eq zero     zero     := inl rfl
+  | has_decidable_eq (succ x) zero     := inr (λ h, nat.no_confusion h)
+  | has_decidable_eq zero     (succ y) := inr (λ h, nat.no_confusion h)
+  | has_decidable_eq (succ x) (succ y) :=
+      if H : x = y
+      then inl (eq.rec_on H rfl)
+      else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
 
   -- less-than is well-founded
   definition lt.wf [instance] : well_founded lt :=
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 835db2507..ad45956ac 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -94,7 +94,7 @@ notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)`
 opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
 
 infixl `;`:15 := and_then
-notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
+notation `[` h `|` r:(foldl `|` (e r, or_else r e) h) `]` := r
 
 definition try         (t : tactic) : tactic := [t | id]
 definition repeat1     (t : tactic) : tactic := t ; repeat t
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 4587b6028..15f90426d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -440,8 +440,8 @@ static void erase_local_binder_info(buffer<expr> & ps) {
         p = update_local(p, binder_info());
 }
 
-static bool is_curr_with_or_comma(parser & p) {
-    return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk());
+static bool is_curr_with_or_comma_or_bar(parser & p) {
+    return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_bar_tk());
 }
 
 /**
@@ -515,6 +515,16 @@ static void throw_invalid_equation_lhs(name const & n, pos_info const & p) {
                        << n << "' in the left-hand-side does not correspond to function(s) being defined", p);
 }
 
+static bool is_eqn_prefix(parser & p) {
+    return p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_comma_tk());
+}
+
+static void check_eqn_prefix(parser & p) {
+    if (!is_eqn_prefix(p))
+        throw parser_error("invalid declaration, ',' or '|' expected", p.pos());
+    p.next();
+}
+
 expr parse_equations(parser & p, name const & n, expr const & type, buffer<name> & auxs,
                      optional<local_environment> const & lenv, buffer<expr> const & ps,
                      pos_info const & def_pos) {
@@ -524,7 +534,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
         parser::local_scope scope1(p, lenv);
         for (expr const & param : ps)
             p.add_local(param);
-        lean_assert(is_curr_with_or_comma(p));
+        lean_assert(is_curr_with_or_comma_or_bar(p));
         fns.push_back(mk_local(n, type));
         if (p.curr_is_token(get_with_tk())) {
             while (p.curr_is_token(get_with_tk())) {
@@ -538,7 +548,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
                 fns.push_back(g);
             }
         }
-        p.check_token_next(get_comma_tk(), "invalid declaration, ',' expected");
+        check_eqn_prefix(p);
         for (expr const & fn : fns)
             p.add_local(fn);
         while (true) {
@@ -574,7 +584,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
                 expr rhs = p.parse_expr();
                 eqns.push_back(Fun(fns, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
             }
-            if (!p.curr_is_token(get_comma_tk()))
+            if (!is_eqn_prefix(p))
                 break;
             p.next();
         }
@@ -594,6 +604,8 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr t  = p.parse_expr();
     p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
+    if (is_eqn_prefix(p))
+        p.next();
     buffer<expr> eqns;
     expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
     while (true) {
@@ -621,7 +633,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
             expr rhs = p.parse_expr();
             eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
         }
-        if (!p.curr_is_token(get_comma_tk()))
+        if (!is_eqn_prefix(p))
             break;
         p.next();
     }
@@ -685,7 +697,7 @@ class definition_cmd_fn {
             m_p.next();
             auto pos = m_p.pos();
             m_type = m_p.parse_expr();
-            if (is_curr_with_or_comma(m_p)) {
+            if (is_curr_with_or_comma_or_bar(m_p)) {
                 m_value = parse_equations(m_p, m_name, m_type, m_aux_decls,
                                           optional<local_environment>(), buffer<expr>(), m_pos);
             } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
@@ -704,7 +716,7 @@ class definition_cmd_fn {
             if (m_p.curr_is_token(get_colon_tk())) {
                 m_p.next();
                 m_type = m_p.parse_scoped_expr(ps, *lenv);
-                if (is_curr_with_or_comma(m_p)) {
+                if (is_curr_with_or_comma_or_bar(m_p)) {
                     m_value = parse_equations(m_p, m_name, m_type, m_aux_decls, lenv, ps, m_pos);
                 } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
                     check_end_of_theorem(m_p);
diff --git a/tests/lean/bad_eqns.lean b/tests/lean/bad_eqns.lean
index 46120bb71..24d97036a 100644
--- a/tests/lean/bad_eqns.lean
+++ b/tests/lean/bad_eqns.lean
@@ -1,15 +1,15 @@
 open nat
 
-definition foo : nat → nat,
-foo (0 + x) := x
+definition foo : nat → nat
+| foo (0 + x) := x
 
-definition foo : nat → nat → nat,
-foo 0 _   := 0,
-foo x ⌞y⌟ := x
+definition foo : nat → nat → nat
+| foo 0 _   := 0
+| foo x ⌞y⌟ := x
 
-definition foo : nat → nat → nat,
-foo 0   _ := 0,
-foo ⌞x⌟ x := x
+definition foo : nat → nat → nat
+| foo 0   _ := 0
+| foo ⌞x⌟ x := x
 
 inductive tree (A : Type) :=
 node   : tree_list A → tree A,
@@ -19,18 +19,18 @@ 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,
-is_leaf (tree.node _)            := bool.ff,
-is_leaf (tree.leaf _)            := bool.tt,
-is_leaf_aux tree_list.nil        := bool.ff,
-is_leaf_aux (tree_list.cons _ _) := bool.ff
+with is_leaf_aux : tree_list A → bool
+| is_leaf (tree.node _)            := bool.ff
+| is_leaf (tree.leaf _)            := bool.tt
+| is_leaf_aux tree_list.nil        := bool.ff
+| is_leaf_aux (tree_list.cons _ _) := bool.ff
 
-definition foo : nat → nat,
-foo 0     := 0,
-foo (x+1) := let y := x + 2 in y * y
+definition foo : nat → nat
+| foo 0     := 0
+| foo (x+1) := let y := x + 2 in y * y
 
 example : foo 5 = 36 := rfl
 
-definition boo : nat → nat,
-boo (x + 1) := boo (x + 2),
-boo 0       := 0
+definition boo : nat → nat
+| boo (x + 1) := boo (x + 2)
+| boo 0       := 0
diff --git a/tests/lean/bad_eqns.lean.expected.out b/tests/lean/bad_eqns.lean.expected.out
index 5fc82a487..36fb4ce97 100644
--- a/tests/lean/bad_eqns.lean.expected.out
+++ b/tests/lean/bad_eqns.lean.expected.out
@@ -1,8 +1,8 @@
-bad_eqns.lean:4:0: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
+bad_eqns.lean:4:2: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
   0 + x
 in the following equation left-hand-side
   foo (0 + x)
-bad_eqns.lean:8:0: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
+bad_eqns.lean:8:2: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
   foo x y
 bad_eqns.lean:10:11: error: invalid recursive equations for 'foo', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
 bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
diff --git a/tests/lean/hott/def_bug1.hlean b/tests/lean/hott/def_bug1.hlean
index 90602b41c..f37e9c921 100644
--- a/tests/lean/hott/def_bug1.hlean
+++ b/tests/lean/hott/def_bug1.hlean
@@ -2,13 +2,13 @@ open eq eq.ops
 
 variable {A : Type}
 
-definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z,
-trans (refl a) (refl a) := refl a
+definition trans : Π {x y z : A} (p : x = y) (q : y = z), x = z
+| trans (refl a) (refl a) := refl a
 
 set_option pp.purify_locals false
 
-definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q,
-con_inv_cancel_left (refl a) (refl a) := refl (refl a)
+definition con_inv_cancel_left : Π {x y z : A} (p : x = y) (q : x = z), p ⬝ (p⁻¹ ⬝ q) = q
+| con_inv_cancel_left (refl a) (refl a) := refl (refl a)
 
-definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q,
-inv_con_cancel_left (refl a) (refl a) := refl (refl a)
+definition inv_con_cancel_left : Π {x y z : A} (p : x = y) (q : y = z), p⁻¹ ⬝ (p ⬝ q) = q
+| inv_con_cancel_left (refl a) (refl a) := refl (refl a)
diff --git a/tests/lean/hott/eq1.hlean b/tests/lean/hott/eq1.hlean
index 420bb851e..db5913e40 100644
--- a/tests/lean/hott/eq1.hlean
+++ b/tests/lean/hott/eq1.hlean
@@ -6,8 +6,8 @@ cons   : Π {n}, A → vector A n → vector A (succ n)
 
 infixr `::` := vector.cons
 
-definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
-swap (a :: b :: vs) := b :: a :: vs
+definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))
+| swap (a :: b :: vs) := b :: a :: vs
 
 -- Remark: in the current approach for HoTT, the equation
 --    swap (a :: b :: v) = b :: a :: v
diff --git a/tests/lean/nonexhaustive.lean b/tests/lean/nonexhaustive.lean
index 2c8f0cc77..9a83af941 100644
--- a/tests/lean/nonexhaustive.lean
+++ b/tests/lean/nonexhaustive.lean
@@ -3,12 +3,12 @@ open nat vector
 
 variable {A : Type}
 
-definition foo : Π {n : nat}, vector A n → nat,
-foo nil           := 0,
-foo (a :: b :: v) := 0
+definition foo : Π {n : nat}, vector A n → nat
+| foo nil           := 0
+| foo (a :: b :: v) := 0
 
 set_option pp.implicit false
 
-definition foo : Π {n : nat}, vector A n → nat,
-foo nil           := 0,
-foo (a :: b :: v) := 0
+definition foo : Π {n : nat}, vector A n → nat
+| foo nil           := 0
+| foo (a :: b :: v) := 0
diff --git a/tests/lean/place_eqn.lean b/tests/lean/place_eqn.lean
index 481ae9dce..40bcc3969 100644
--- a/tests/lean/place_eqn.lean
+++ b/tests/lean/place_eqn.lean
@@ -1,5 +1,5 @@
 open nat
 
-definition foo : nat → nat,
-foo zero     := _,
-foo (succ a) := _
+definition foo : nat → nat
+| foo zero     := _
+| foo (succ a) := _
diff --git a/tests/lean/place_eqn.lean.expected.out b/tests/lean/place_eqn.lean.expected.out
index 720029ccb..8d45277e2 100644
--- a/tests/lean/place_eqn.lean.expected.out
+++ b/tests/lean/place_eqn.lean.expected.out
@@ -1,7 +1,7 @@
-place_eqn.lean:4:16: error: don't know how to synthesize placeholder
+place_eqn.lean:4:18: error: don't know how to synthesize placeholder
 foo : ℕ → ℕ
 ⊢ ℕ
-place_eqn.lean:5:16: error: don't know how to synthesize placeholder
+place_eqn.lean:5:18: error: don't know how to synthesize placeholder
 foo : ℕ → ℕ,
 a : ℕ
 ⊢ ℕ
diff --git a/tests/lean/run/assert_tac2.lean b/tests/lean/run/assert_tac2.lean
index d4af16165..f643eadc9 100644
--- a/tests/lean/run/assert_tac2.lean
+++ b/tests/lean/run/assert_tac2.lean
@@ -3,12 +3,12 @@ open nat eq.ops
 
 theorem lcm_dvd {m n k : nat} (H1 : (m | k)) (H2 : (n | k)) : (lcm m n | k) :=
 match eq_zero_or_pos k with
-  @or.inl _ _ kzero :=
+| @or.inl _ _ kzero :=
     begin
       rewrite kzero,
       apply dvd_zero
-    end,
-  @or.inr _ _ kpos  :=
+    end
+| @or.inr _ _ kpos  :=
     obtain (p : nat) (km : k = m * p), from exists_eq_mul_right_of_dvd H1,
     obtain (q : nat) (kn : k = n * q), from exists_eq_mul_right_of_dvd H2,
     begin
diff --git a/tests/lean/run/eq1.lean b/tests/lean/run/eq1.lean
index 5ba3494ce..8f278dd5a 100644
--- a/tests/lean/run/eq1.lean
+++ b/tests/lean/run/eq1.lean
@@ -3,14 +3,14 @@ monday, tuesday, wednesday, thursday, friday, saturday, sunday
 
 open day
 
-definition next_weekday : day → day,
-next_weekday monday    := tuesday,
-next_weekday tuesday   := wednesday,
-next_weekday wednesday := thursday,
-next_weekday thursday  := friday,
-next_weekday friday    := monday,
-next_weekday saturday  := monday,
-next_weekday sunday    := monday
+definition next_weekday : day → day
+| next_weekday monday    := tuesday
+| next_weekday tuesday   := wednesday
+| next_weekday wednesday := thursday
+| next_weekday thursday  := friday
+| next_weekday friday    := monday
+| next_weekday saturday  := monday
+| next_weekday sunday    := monday
 
 example : next_weekday (next_weekday monday) = wednesday :=
 rfl
diff --git a/tests/lean/run/eq10.lean b/tests/lean/run/eq10.lean
index 2bd4bf768..f87832c01 100644
--- a/tests/lean/run/eq10.lean
+++ b/tests/lean/run/eq10.lean
@@ -9,13 +9,13 @@ allf : (nat → formula) → formula
 namespace formula
   definition implies (a b : Prop) : Prop := a → b
 
-  definition denote : formula → Prop,
-  denote (eqf n1 n2)  := n1 = n2,
-  denote (andf f1 f2) := denote f1 ∧ denote f2,
-  denote (impf f1 f2) := implies (denote f1) (denote f2),
-  denote (orf f1 f2)  := denote f1 ∨ denote f2,
-  denote (notf f)     := ¬ denote f,
-  denote (allf f)     := ∀ n : nat, denote (f n)
+  definition denote : formula → Prop
+  | denote (eqf n1 n2)  := n1 = n2
+  | denote (andf f1 f2) := denote f1 ∧ denote f2
+  | denote (impf f1 f2) := implies (denote f1) (denote f2)
+  | denote (orf f1 f2)  := denote f1 ∨ denote f2
+  | denote (notf f)     := ¬ denote f
+  | denote (allf f)     := ∀ n : nat, denote (f n)
 
   theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
   rfl
diff --git a/tests/lean/run/eq11.lean b/tests/lean/run/eq11.lean
index c1f123f56..a15ab186f 100644
--- a/tests/lean/run/eq11.lean
+++ b/tests/lean/run/eq11.lean
@@ -3,12 +3,12 @@ monday, tuesday, wednesday, thursday, friday, saturday, sunday
 
 open day
 
-definition next_weekday : day → day,
-next_weekday monday    := tuesday,
-next_weekday tuesday   := wednesday,
-next_weekday wednesday := thursday,
-next_weekday thursday  := friday,
-next_weekday _         := monday
+definition next_weekday : day → day
+| next_weekday monday    := tuesday
+| next_weekday tuesday   := wednesday
+| next_weekday wednesday := thursday
+| next_weekday thursday  := friday
+| next_weekday _         := monday
 
 theorem next_weekday_monday    : next_weekday monday    = tuesday   := rfl
 theorem next_weekday_tuesday   : next_weekday tuesday   = wednesday := rfl
diff --git a/tests/lean/run/eq12.lean b/tests/lean/run/eq12.lean
index 1b6310b51..5bc9830f6 100644
--- a/tests/lean/run/eq12.lean
+++ b/tests/lean/run/eq12.lean
@@ -1,10 +1,10 @@
 open nat bool inhabited
 
-definition diag : bool → bool → bool → nat,
-diag _  tt ff := 1,
-diag ff _  tt := 2,
-diag tt ff _  := 3,
-diag _  _  _  := arbitrary nat
+definition diag : bool → bool → bool → nat
+| diag _  tt ff := 1
+| diag ff _  tt := 2
+| diag tt ff _  := 3
+| diag _  _  _  := arbitrary nat
 
 theorem diag1 (a : bool) : diag a tt ff = 1 :=
 bool.cases_on a rfl rfl
diff --git a/tests/lean/run/eq13.lean b/tests/lean/run/eq13.lean
index 92f25ee9d..d9f676e3b 100644
--- a/tests/lean/run/eq13.lean
+++ b/tests/lean/run/eq13.lean
@@ -1,13 +1,13 @@
 open nat
 
-definition f : nat → nat → nat,
-f _ 0 := 0,
-f 0 _ := 1,
-f _ _ := arbitrary nat
+definition f : nat → nat → nat
+| f _ 0 := 0
+| f 0 _ := 1
+| f _ _ := arbitrary nat
 
-theorem f_zero_right : ∀ a, f a 0 = 0,
-f_zero_right 0        := rfl,
-f_zero_right (succ _) := rfl
+theorem f_zero_right : ∀ a, f a 0 = 0
+| f_zero_right 0        := rfl
+| f_zero_right (succ _) := rfl
 
 theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
 rfl
diff --git a/tests/lean/run/eq14.lean b/tests/lean/run/eq14.lean
index 11552c6a3..9ec62b385 100644
--- a/tests/lean/run/eq14.lean
+++ b/tests/lean/run/eq14.lean
@@ -1,13 +1,13 @@
 open nat decidable
 
-definition has_decidable_eq : ∀ a b : nat, decidable (a = b),
-has_decidable_eq 0     0     := inl rfl,
-has_decidable_eq (a+1) 0     := inr (λ h, nat.no_confusion h),
-has_decidable_eq 0     (b+1) := inr (λ h, nat.no_confusion h),
-has_decidable_eq (a+1) (b+1) :=
-  if H : a = b
-  then inl (eq.rec_on H rfl)
-  else inr (λ h : a+1 = b+1, nat.no_confusion h (λ e : a = b, absurd e H))
+definition has_decidable_eq : ∀ a b : nat, decidable (a = b)
+| has_decidable_eq 0     0     := inl rfl
+| has_decidable_eq (a+1) 0     := inr (λ h, nat.no_confusion h)
+| has_decidable_eq 0     (b+1) := inr (λ h, nat.no_confusion h)
+| has_decidable_eq (a+1) (b+1) :=
+    if H : a = b
+    then inl (eq.rec_on H rfl)
+    else inr (λ h : a+1 = b+1, nat.no_confusion h (λ e : a = b, absurd e H))
 
 check has_decidable_eq
 print definition has_decidable_eq
diff --git a/tests/lean/run/eq15.lean b/tests/lean/run/eq15.lean
index 10671d8b2..7e695acf9 100644
--- a/tests/lean/run/eq15.lean
+++ b/tests/lean/run/eq15.lean
@@ -3,9 +3,9 @@ open list
 
 set_option pp.implicit true
 
-definition append : Π {A : Type}, list A → list A → list A,
-append nil      l := l,
-append (h :: t) l := h :: (append t l)
+definition append : Π {A : Type}, list A → list A → list A
+| append nil      l := l
+| append (h :: t) l := h :: (append t l)
 
 theorem append_nil {A : Type} (l : list A) : append nil l = l :=
 rfl
diff --git a/tests/lean/run/eq16.lean b/tests/lean/run/eq16.lean
index 284f773ae..23e68b163 100644
--- a/tests/lean/run/eq16.lean
+++ b/tests/lean/run/eq16.lean
@@ -4,9 +4,9 @@ open list
 variable {A : Type}
 set_option pp.implicit true
 
-definition append : list A → list A → list A,
-append nil      l := l,
-append (h :: t) l := h :: (append t l)
+definition append : list A → list A → list A
+| append nil      l := l
+| append (h :: t) l := h :: (append t l)
 
 theorem append_nil (l : list A) : append nil l = l :=
 rfl
diff --git a/tests/lean/run/eq17.lean b/tests/lean/run/eq17.lean
index db084c752..c704120dc 100644
--- a/tests/lean/run/eq17.lean
+++ b/tests/lean/run/eq17.lean
@@ -1,5 +1,5 @@
 open nat
 
-definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b,
-lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a)),
-lt_of_succ (lt.step h)        := lt.step  (lt_of_succ h)
+definition lt_of_succ : ∀ {a b : nat}, succ a < b → a < b
+| lt_of_succ (lt.base (succ a)) := lt.trans (lt.base a) (lt.base (succ a))
+| lt_of_succ (lt.step h)        := lt.step  (lt_of_succ h)
diff --git a/tests/lean/run/eq18.lean b/tests/lean/run/eq18.lean
index cbc147156..1073158ef 100644
--- a/tests/lean/run/eq18.lean
+++ b/tests/lean/run/eq18.lean
@@ -1,9 +1,9 @@
 import data.vector
 open nat vector
 
-definition last {A : Type} : Π {n}, vector A (succ n) → A,
-last (a :: nil) := a,
-last (a :: v)   := last v
+definition last {A : Type} : Π {n}, vector A (succ n) → A
+| last (a :: nil) := a
+| last (a :: v)   := last v
 
 theorem last_cons_nil {A : Type} {n : nat} (a : A) : last (a :: nil) = a :=
 rfl
diff --git a/tests/lean/run/eq19.lean b/tests/lean/run/eq19.lean
index 2e526ec21..d695c6903 100644
--- a/tests/lean/run/eq19.lean
+++ b/tests/lean/run/eq19.lean
@@ -3,9 +3,9 @@ open nat vector prod
 
 variables {A B : Type}
 
-definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n,
-unzip nil           := (nil, nil),
-unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
+definition unzip : Π {n}, vector (A × B) n → vector A n × vector B n
+| unzip nil           := (nil, nil)
+| unzip ((a, b) :: t) := (a :: pr₁ (unzip t), b :: pr₂ (unzip t))
 
 theorem unzip_nil : unzip nil = (@nil A, @nil B) :=
 rfl
diff --git a/tests/lean/run/eq2.lean b/tests/lean/run/eq2.lean
index 2ecc6a4a4..f3639b0aa 100644
--- a/tests/lean/run/eq2.lean
+++ b/tests/lean/run/eq2.lean
@@ -1,5 +1,5 @@
-definition symm {A : Type} : Π {a b : A}, a = b → b = a,
-symm rfl := rfl
+definition symm {A : Type} : Π {a b : A}, a = b → b = a
+| symm rfl := rfl
 
-definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c,
-trans rfl rfl := rfl
+definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
+| trans rfl rfl := rfl
diff --git a/tests/lean/run/eq20.lean b/tests/lean/run/eq20.lean
index 1ca5a107f..a953a9d98 100644
--- a/tests/lean/run/eq20.lean
+++ b/tests/lean/run/eq20.lean
@@ -7,9 +7,9 @@ context
   parameter [H : decidable_pred p]
   include H
 
-  definition filter : list A → list A,
-  filter nil      := nil,
-  filter (a :: l) := if p a then a :: filter l else filter l
+  definition filter : list A → list A
+  | filter nil      := nil
+  | filter (a :: l) := if p a then a :: filter l else filter l
 
   theorem filter_nil : filter nil = nil :=
   rfl
diff --git a/tests/lean/run/eq21.lean b/tests/lean/run/eq21.lean
index d4618acf4..e61c2b491 100644
--- a/tests/lean/run/eq21.lean
+++ b/tests/lean/run/eq21.lean
@@ -3,9 +3,9 @@ eqf  : nat → nat → formula,
 impf : formula → formula → formula
 
 namespace formula
-  definition denote : formula → Prop,
-  denote (eqf n1 n2)  := n1 = n2,
-  denote (impf f1 f2) := denote f1 → denote f2
+  definition denote : formula → Prop
+  | denote (eqf n1 n2)  := n1 = n2
+  | denote (impf f1 f2) := denote f1 → denote f2
 
   theorem denote_eqf (n1 n2 : nat) : denote (eqf n1 n2) = (n1 = n2) :=
   rfl
diff --git a/tests/lean/run/eq22.lean b/tests/lean/run/eq22.lean
index fae15af6a..dd313877e 100644
--- a/tests/lean/run/eq22.lean
+++ b/tests/lean/run/eq22.lean
@@ -1,9 +1,9 @@
 import data.list
 open list
 
-definition head {A : Type} : Π (l : list A), l ≠ nil → A,
-head nil h      := absurd rfl h,
-head (a :: l) _ := a
+definition head {A : Type} : Π (l : list A), l ≠ nil → A
+| head nil h      := absurd rfl h
+| head (a :: l) _ := a
 
 theorem head_cons {A : Type} (a : A) (l : list A) (h : a :: l ≠ nil) : head (a :: l) h = a :=
 rfl
diff --git a/tests/lean/run/eq23.lean b/tests/lean/run/eq23.lean
index e1a44aafc..1c4afcaee 100644
--- a/tests/lean/run/eq23.lean
+++ b/tests/lean/run/eq23.lean
@@ -9,9 +9,9 @@ cons : tree A → tree_list A → tree_list A
 
 namespace tree_list
 
-definition len {A : Type} : tree_list A → nat,
-len (nil A)    := 0,
-len (cons t l) := len l + 1
+definition len {A : Type} : tree_list A → nat
+| len (nil A)    := 0
+| len (cons t l) := len l + 1
 
 theorem len_nil {A : Type} : len (nil A) = 0 :=
 rfl
diff --git a/tests/lean/run/eq24.lean b/tests/lean/run/eq24.lean
index c5d3b7b97..b827e8e60 100644
--- a/tests/lean/run/eq24.lean
+++ b/tests/lean/run/eq24.lean
@@ -11,11 +11,11 @@ namespace tree
 open tree_list
 
 definition size {A : Type} : tree A → nat
-with size_l                : tree_list A → nat,
-size (leaf a)     := 1,
-size (node l)     := size_l l,
-size_l !nil       := 0,
-size_l (cons t l) := size t + size_l l
+with size_l                : tree_list A → nat
+| size (leaf a)     := 1
+| size (node l)     := size_l l
+| size_l !nil       := 0
+| size_l (cons t l) := size t + size_l l
 
 variables {A : Type}
 
@@ -32,13 +32,13 @@ theorem size_l_cons (t : tree A) (l : tree_list A) : size_l (cons t l) = size t
 rfl
 
 definition eq_tree {A : Type} : tree A → tree A → Prop
-with eq_tree_list             : tree_list A → tree_list A → Prop,
-eq_tree (leaf a₁) (leaf a₂)            := a₁ = a₂,
-eq_tree (node l₁) (node l₂)            := eq_tree_list l₁ l₂,
-eq_tree _ _                            := false,
-eq_tree_list !nil !nil                 := true,
-eq_tree_list (cons t₁ l₁) (cons t₂ l₂) := eq_tree t₁ t₂ ∧ eq_tree_list l₁ l₂,
-eq_tree_list _ _                       := false
+with eq_tree_list             : tree_list A → tree_list A → Prop
+| eq_tree (leaf a₁) (leaf a₂)            := a₁ = a₂
+| eq_tree (node l₁) (node l₂)            := eq_tree_list l₁ l₂
+| eq_tree _ _                            := false
+| eq_tree_list !nil !nil                 := true
+| eq_tree_list (cons t₁ l₁) (cons t₂ l₂) := eq_tree t₁ t₂ ∧ eq_tree_list l₁ l₂
+| eq_tree_list _ _                       := false
 
 theorem eq_tree_leaf (a₁ a₂ : A) : eq_tree (leaf a₁) (leaf a₂) = (a₁ = a₂) :=
 rfl
diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean
index 823ac0e6d..2768472f0 100644
--- a/tests/lean/run/eq25.lean
+++ b/tests/lean/run/eq25.lean
@@ -6,6 +6,6 @@ definition Nat := N
 
 open N
 
-definition add : Nat → Nat → Nat,
-add O     b := b,
-add (S a) b := S (add a b)
+definition add : Nat → Nat → Nat
+| add O     b := b
+| add (S a) b := S (add a b)
diff --git a/tests/lean/run/eq3.lean b/tests/lean/run/eq3.lean
index a1e405782..b281d7290 100644
--- a/tests/lean/run/eq3.lean
+++ b/tests/lean/run/eq3.lean
@@ -1,8 +1,8 @@
 import data.vector
 open nat vector
 
-definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n)),
-swap (a :: b :: vs) := b :: a :: vs
+definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))
+| swap (a :: b :: vs) := b :: a :: vs
 
 example (n : nat) (a b : num) (v : vector num n) : swap (a :: b :: v) = b :: a :: v :=
 rfl
diff --git a/tests/lean/run/eq4.lean b/tests/lean/run/eq4.lean
index 221adb043..923c97005 100644
--- a/tests/lean/run/eq4.lean
+++ b/tests/lean/run/eq4.lean
@@ -1,9 +1,9 @@
 open nat
 
-definition half : nat → nat,
-half 0     := 0,
-half 1     := 0,
-half (x+2) := half x + 1
+definition half : nat → nat
+| half 0     := 0
+| half 1     := 0
+| half (x+2) := half x + 1
 
 theorem half0 : half 0 = 0 :=
 rfl
diff --git a/tests/lean/run/eq5.lean b/tests/lean/run/eq5.lean
index 62186f0cf..cd555faeb 100644
--- a/tests/lean/run/eq5.lean
+++ b/tests/lean/run/eq5.lean
@@ -1,9 +1,9 @@
 open nat
 
-definition fib : nat → nat,
-fib 0     := 1,
-fib 1     := 1,
-fib (x+2) := fib x + fib (x+1)
+definition fib : nat → nat
+| fib 0     := 1
+| fib 1     := 1
+| fib (x+2) := fib x + fib (x+1)
 
 theorem fib0 : fib 0 = 1 :=
 rfl
diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean
index 1a8784f4d..fbd73ecae 100644
--- a/tests/lean/run/eq6.lean
+++ b/tests/lean/run/eq6.lean
@@ -1,9 +1,9 @@
 import data.list
 open list
 
-definition append {A : Type} : list A → list A → list A,
-append nil      l := l,
-append (h :: t) l := h :: (append t l)
+definition append {A : Type} : list A → list A → list A
+| append nil      l := l
+| append (h :: t) l := h :: (append t l)
 
 theorem append_nil {A : Type} (l : list A) : append nil l = l :=
 rfl
diff --git a/tests/lean/run/eq7.lean b/tests/lean/run/eq7.lean
index a98f79991..aa20d9189 100644
--- a/tests/lean/run/eq7.lean
+++ b/tests/lean/run/eq7.lean
@@ -1,9 +1,9 @@
 import data.vector
 open nat vector
 
-definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n,
-diag nil               := nil,
-diag ((a :: va) :: vs) := a :: diag (map tail vs)
+definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n
+| diag nil               := nil
+| diag ((a :: va) :: vs) := a :: diag (map tail vs)
 
 theorem diag_nil (A : Type) : diag (@nil (vector A 0)) = nil :=
 rfl
diff --git a/tests/lean/run/eq8.lean b/tests/lean/run/eq8.lean
index 6e76166ed..3f4d99aca 100644
--- a/tests/lean/run/eq8.lean
+++ b/tests/lean/run/eq8.lean
@@ -1,6 +1,6 @@
 import data.vector
 open vector
 
-definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n,
-map nil nil             := nil,
-map (a :: va) (b :: vb) := f a b :: map va vb
+definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n
+| map nil nil             := nil
+| map (a :: va) (b :: vb) := f a b :: map va vb
diff --git a/tests/lean/run/eq9.lean b/tests/lean/run/eq9.lean
index cf968c068..6443bacfc 100644
--- a/tests/lean/run/eq9.lean
+++ b/tests/lean/run/eq9.lean
@@ -1,9 +1,9 @@
 open nat
 
-theorem lt_trans : ∀ {a b c : nat}, a < b → b < c → a < c,
-lt_trans h  (lt.base _)   := lt.step h,
-lt_trans h₁ (lt.step h₂)  := lt.step (lt_trans h₁ h₂)
+theorem lt_trans : ∀ {a b c : nat}, a < b → b < c → a < c
+| lt_trans h  (lt.base _)   := lt.step h
+| lt_trans h₁ (lt.step h₂)  := lt.step (lt_trans h₁ h₂)
 
-theorem lt_succ : ∀ {a b : nat}, a < b → succ a < succ b,
-lt_succ (lt.base a)  := lt.base (succ a),
-lt_succ (lt.step h)  := lt.step (lt_succ h)
+theorem lt_succ : ∀ {a b : nat}, a < b → succ a < succ b
+| lt_succ (lt.base a)  := lt.base (succ a)
+| lt_succ (lt.step h)  := lt.step (lt_succ h)
diff --git a/tests/lean/run/eqn_tac.lean b/tests/lean/run/eqn_tac.lean
index 24b2504b9..6b9e9903e 100644
--- a/tests/lean/run/eqn_tac.lean
+++ b/tests/lean/run/eqn_tac.lean
@@ -1,15 +1,15 @@
 open nat
 
-definition foo : nat → nat,
-foo zero     := begin exact zero end,
-foo (succ a) := begin exact a end
+definition foo : nat → nat
+| foo zero     := begin exact zero end
+| foo (succ a) := begin exact a end
 
 example : foo zero = zero := rfl
 example (a : nat) : foo (succ a) = a := rfl
 
-definition bla : nat → nat,
-bla zero := zero,
-bla (succ a) :=
+definition bla : nat → nat
+| bla zero := zero
+| bla (succ a) :=
   begin
     apply foo,
     exact a
diff --git a/tests/lean/run/finbug.lean b/tests/lean/run/finbug.lean
index 4a6430828..c1819b2bd 100644
--- a/tests/lean/run/finbug.lean
+++ b/tests/lean/run/finbug.lean
@@ -14,18 +14,18 @@ fz : Π n, fin (succ n),
 fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
-  definition to_nat : Π {n}, fin n → nat,
-  to_nat (fz n) := zero,
-  to_nat (@fs n f) := succ (@to_nat n f)
+  definition to_nat : Π {n}, fin n → nat
+  | to_nat (fz n) := zero
+  | to_nat (@fs n f) := succ (@to_nat n f)
 
-  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n),
-  lift (fz n)     m := fz (add m n),
-  lift (@fs n f)  m := fs (@lift n f m)
+  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
+  | lift (fz n)     m := fz (add m n)
+  | lift (@fs n f)  m := fs (@lift n f m)
 
-  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
-  to_nat_lift (fz n) m    := rfl,
-  to_nat_lift (@fs n f) m := calc
-     to_nat (fs f) = (to_nat f) + 1           : rfl
-              ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
-              ...  = to_nat (lift (fs f) m)   : rfl
+  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
+  | to_nat_lift (fz n) m    := rfl
+  | to_nat_lift (@fs n f) m := calc
+       to_nat (fs f) = (to_nat f) + 1           : rfl
+                ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
+                ...  = to_nat (lift (fs f) m)   : rfl
 end fin
diff --git a/tests/lean/run/finbug2.lean b/tests/lean/run/finbug2.lean
index a67f5c71b..cc8978177 100644
--- a/tests/lean/run/finbug2.lean
+++ b/tests/lean/run/finbug2.lean
@@ -14,18 +14,18 @@ fz : Π n, fin (succ n),
 fs : Π {n}, fin n → fin (succ n)
 
 namespace fin
-  definition to_nat : Π {n}, fin n → nat,
-  @to_nat (succ n) (fz n) := zero,
-  @to_nat (succ n) (fs f) := succ (@to_nat n f)
+  definition to_nat : Π {n}, fin n → nat
+  | @to_nat (succ n) (fz n) := zero
+  | @to_nat (succ n) (fs f) := succ (@to_nat n f)
 
-  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n),
-  @lift (succ n) (fz n)     m := fz (add m n),
-  @lift (succ n) (@fs n f)  m := fs (@lift n f m)
+  definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
+  | @lift (succ n) (fz n)     m := fz (add m n)
+  | @lift (succ n) (@fs n f)  m := fs (@lift n f m)
 
-  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m),
-  to_nat_lift (fz n) m    := rfl,
-  to_nat_lift (@fs n f) m := calc
-     to_nat (fs f) = (to_nat f) + 1           : rfl
-              ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
-              ...  = to_nat (lift (fs f) m)   : rfl
+  theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
+  | to_nat_lift (fz n) m    := rfl
+  | to_nat_lift (@fs n f) m := calc
+      to_nat (fs f) = (to_nat f) + 1           : rfl
+               ...  = (to_nat (lift f m)) + 1  : to_nat_lift f
+               ...  = to_nat (lift (fs f) m)   : rfl
 end fin
diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean
index ed891ef29..1f903778e 100644
--- a/tests/lean/run/match3.lean
+++ b/tests/lean/run/match3.lean
@@ -3,22 +3,22 @@ open nat
 
 definition foo (a : nat) : nat :=
 match a with
- zero   := zero,
- succ n := n
+| zero   := zero
+| succ n := n
 end
 
 example : foo 3 = 2 := rfl
 
 open decidable
 
-protected theorem dec_eq : ∀ x y : nat, decidable (x = y),
-dec_eq zero     zero     := inl rfl,
-dec_eq (succ x) zero     := inr (λ h, nat.no_confusion h),
-dec_eq zero     (succ y) := inr (λ h, nat.no_confusion h),
-dec_eq (succ x) (succ y) :=
+protected theorem dec_eq : ∀ x y : nat, decidable (x = y)
+| dec_eq zero     zero     := inl rfl
+| dec_eq (succ x) zero     := inr (λ h, nat.no_confusion h)
+| dec_eq zero     (succ y) := inr (λ h, nat.no_confusion h)
+| dec_eq (succ x) (succ y) :=
   match dec_eq x y with
-    inl H := inl (eq.rec_on H rfl),
-    inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
+  | inl H := inl (eq.rec_on H rfl)
+  | inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
   end
 
 context
@@ -28,12 +28,12 @@ context
   parameter [H : decidable_pred p]
   include H
 
-  definition filter : list A → list A,
-  filter nil      := nil,
-  filter (a :: l) :=
+  definition filter : list A → list A
+  | filter nil      := nil
+  | filter (a :: l) :=
     match H a with
-     inl h := a :: filter l,
-     inr h := filter l
+    | inl h := a :: filter l
+    | inr h := filter l
     end
 
   theorem filter_nil : filter nil = nil :=
@@ -45,9 +45,9 @@ end
 
 definition sub2 (a : nat) : nat :=
 match a with
- 0   := 0,
- 1   := 0,
- b+2 := b
+| 0   := 0
+| 1   := 0
+| b+2 := b
 end
 
 example (a : nat) : sub2 (succ (succ a)) = a := rfl
diff --git a/tests/lean/run/match4.lean b/tests/lean/run/match4.lean
index 4aa55c10d..e4ae30904 100644
--- a/tests/lean/run/match4.lean
+++ b/tests/lean/run/match4.lean
@@ -2,10 +2,10 @@ open nat bool inhabited prod
 
 definition diag (a b c : bool) : nat :=
 match (a, b, c) with
-  (_,  tt, ff) := 1,
-  (ff, _,  tt) := 2,
-  (tt, ff, _)  := 3,
-  (_,  _,  _)  := arbitrary nat
+  | (_,  tt, ff) := 1
+  | (ff, _,  tt) := 2
+  | (tt, ff, _)  := 3
+  | (_,  _,  _)  := arbitrary nat
 end
 
 theorem diag1 (a : bool) : diag a tt ff = 1 :=
diff --git a/tests/lean/run/sigma_match.lean b/tests/lean/run/sigma_match.lean
index 606166a96..3a647e86a 100644
--- a/tests/lean/run/sigma_match.lean
+++ b/tests/lean/run/sigma_match.lean
@@ -10,8 +10,8 @@ match x with
   ⟨a, b, h⟩ := a
 end
 
-definition src2 {A B : Type} : arrow_ob A B → A,
-src2 ⟨a, _, _⟩ := a
+definition src2 {A B : Type} : arrow_ob A B → A
+| src2 ⟨a, _, _⟩ := a
 
 definition src3 {A B : Type} (x : arrow_ob A B) : A :=
 match x with
diff --git a/tests/lean/run/unzip_bug.lean b/tests/lean/run/unzip_bug.lean
index 281074b68..c71656dc5 100644
--- a/tests/lean/run/unzip_bug.lean
+++ b/tests/lean/run/unzip_bug.lean
@@ -3,9 +3,9 @@ open nat vector prod
 
 variables {A B : Type}
 
-definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
-@unzip ⌞zero⌟   nil           := (nil, nil),
-@unzip ⌞succ n⌟ ((a, b) :: v) :=
+definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
+| @unzip ⌞zero⌟   nil           := (nil, nil)
+| @unzip ⌞succ n⌟ ((a, b) :: v) :=
   match unzip v with
    (va, vb) := (a :: va, b :: vb)
   end
diff --git a/tests/lean/shadow.lean b/tests/lean/shadow.lean
index dc54137f3..4651afca1 100644
--- a/tests/lean/shadow.lean
+++ b/tests/lean/shadow.lean
@@ -3,6 +3,6 @@ open nat
 variable a : nat
 
 -- The variable 'a' in the following definition is not the variable 'a' above
-definition tadd : nat → nat → nat,
-tadd zero     b := b,
-tadd (succ a) b := succ (tadd a b)
+definition tadd : nat → nat → nat
+| tadd zero     b := b
+| tadd (succ a) b := succ (tadd a b)
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index c80db5659..a1a8c1790 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/tests/lean/shadow.lean.expected.out
@@ -1 +1 @@
-shadow.lean:8:11: error: invalid recursive equation, variable 'a' has the same name of a variable in an outer-scope (solution: rename this variable)
+shadow.lean:8:13: error: invalid recursive equation, variable 'a' has the same name of a variable in an outer-scope (solution: rename this variable)
diff --git a/tests/lean/unzip_error.lean b/tests/lean/unzip_error.lean
index 183e26ada..6cd44ffcd 100644
--- a/tests/lean/unzip_error.lean
+++ b/tests/lean/unzip_error.lean
@@ -3,9 +3,9 @@ open nat vector prod
 
 variables {A B : Type}
 
-definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
-unzip  nil          := (nil, nil),
-unzip ((a, b) :: v) :=
+definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n
+| unzip  nil          := (nil, nil)
+| unzip ((a, b) :: v) :=
   match unzip v with
     (va, vb) := (a :: va, b :: vb)
   end