From 661e681ac9d003ea50f8faa6cb820188d44ae09e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 17 Jul 2014 20:47:33 +0100
Subject: [PATCH] feat(frontends/lean/decl_cmds): allow parameters with
 different types to be declared using the same 'parameters' command

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/decl_cmds.cpp | 48 ++++++++++++++++++--------------
 1 file changed, 27 insertions(+), 21 deletions(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index eb8f0a03c0..d20ccb5c12 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -302,30 +302,36 @@ environment theorem_cmd(parser & p) {
     return definition_cmd_core(p, true, true);
 }
 
+static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("[");
+
 static environment variables_cmd(parser & p) {
     auto pos = p.pos();
-    buffer<name> ids;
-    optional<binder_info> bi = parse_binder_info(p);
-    while (!p.curr_is_token(g_colon)) {
-        name id = p.check_id_next("invalid parameters declaration, identifier expected");
-        check_atomic(id);
-        ids.push_back(id);
-    }
-    p.next();
-    optional<parser::local_scope> scope1;
-    if (!in_section(p.env()))
-        scope1.emplace(p);
-    expr type = p.parse_expr();
-    p.parse_close_binder_info(bi);
-    level_param_names ls = to_level_param_names(collect_univ_params(type));
-    level_param_names new_ls;
-    list<expr> ctx = locals_to_context(type, p);
-    std::tie(type, new_ls) = p.elaborate_type(type, ctx);
-    update_section_local_levels(p, new_ls);
-    ls = append(ls, new_ls);
     environment env = p.env();
-    for (auto id : ids)
-        env = declare_var(p, env, id, ls, type, false, bi, pos);
+    while (true) {
+        optional<binder_info> bi = parse_binder_info(p);
+        buffer<name> ids;
+        while (!p.curr_is_token(g_colon)) {
+            name id = p.check_id_next("invalid parameters declaration, identifier expected");
+            check_atomic(id);
+            ids.push_back(id);
+        }
+        p.next();
+        optional<parser::local_scope> scope1;
+        if (!in_section(p.env()))
+            scope1.emplace(p);
+        expr type = p.parse_expr();
+        p.parse_close_binder_info(bi);
+        level_param_names ls = to_level_param_names(collect_univ_params(type));
+        level_param_names new_ls;
+        list<expr> ctx = locals_to_context(type, p);
+        std::tie(type, new_ls) = p.elaborate_type(type, ctx);
+        update_section_local_levels(p, new_ls);
+        ls = append(ls, new_ls);
+        for (auto id : ids)
+            env = declare_var(p, env, id, ls, type, false, bi, pos);
+        if (!p.curr_is_token(g_lparen) && !p.curr_is_token(g_lcurly) && !p.curr_is_token(g_ldcurly) && !p.curr_is_token(g_lbracket))
+            break;
+    }
     return env;
 }