From 3392aa90b5ec03e05775aba690453a21567d78f1 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 13 Jul 2017 15:14:46 +0100
Subject: [PATCH] fix(frontends/lean/definition_cmds): support parameters in
 mutual defs

---
 src/frontends/lean/definition_cmds.cpp |  1 +
 tests/lean/run/mutual_parameter.lean   | 17 +++++++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/lean/run/mutual_parameter.lean

diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index cb0233f9a9..cfb183dc1d 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -510,6 +510,7 @@ static environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, cmd
         name c_real_name;
         std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name,
                                                         curr_type, some_expr(curr), {}, meta, header_pos);
+        env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
         new_d_names.push_back(c_real_name);
         elab.set_env(env);
     }
diff --git a/tests/lean/run/mutual_parameter.lean b/tests/lean/run/mutual_parameter.lean
new file mode 100644
index 0000000000..ce6640d19b
--- /dev/null
+++ b/tests/lean/run/mutual_parameter.lean
@@ -0,0 +1,17 @@
+section
+parameter (k : ℕ)
+
+mutual def foo, bar
+with foo : ℕ → ℕ
+| 0 := k
+| (n+1) := bar n
+with bar : ℕ → ℕ
+| 0 := k+10
+| (n+1) := foo n
+
+def baz : ℕ := foo 3
+
+def foo' (n : ℕ) := k+n
+def baz' : ℕ := foo' 3
+
+end
\ No newline at end of file