From 75d7e4ab9e229643e52125e48862b6c4240229c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Jan 2015 12:35:29 -0800
Subject: [PATCH] feat(frontends/lean): add 'end' token to match expressions

---
 src/frontends/lean/decl_cmds.cpp | 1 +
 tests/lean/run/match3.lean       | 4 ++++
 tests/lean/run/match4.lean       | 1 +
 3 files changed, 6 insertions(+)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index e9cdb9e97..7e8eb5223 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -497,6 +497,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
             break;
         p.next();
     }
+    p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected");
     expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
     return p.mk_app(f, t, pos);
 }
diff --git a/tests/lean/run/match3.lean b/tests/lean/run/match3.lean
index 56cae9859..ed891ef29 100644
--- a/tests/lean/run/match3.lean
+++ b/tests/lean/run/match3.lean
@@ -5,6 +5,7 @@ definition foo (a : nat) : nat :=
 match a with
  zero   := zero,
  succ n := n
+end
 
 example : foo 3 = 2 := rfl
 
@@ -18,6 +19,7 @@ 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))
+  end
 
 context
   open list
@@ -32,6 +34,7 @@ context
     match H a with
      inl h := a :: filter l,
      inr h := filter l
+    end
 
   theorem filter_nil : filter nil = nil :=
   rfl
@@ -45,5 +48,6 @@ match a with
  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 56c11366d..4aa55c10d 100644
--- a/tests/lean/run/match4.lean
+++ b/tests/lean/run/match4.lean
@@ -6,6 +6,7 @@ match (a, b, c) with
   (ff, _,  tt) := 2,
   (tt, ff, _)  := 3,
   (_,  _,  _)  := arbitrary nat
+end
 
 theorem diag1 (a : bool) : diag a tt ff = 1 :=
 bool.cases_on a rfl rfl