From dc2ac92846e174866c399d00c8ae63723e336595 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Feb 2015 21:33:52 -0800
Subject: [PATCH] fix(library/definitional/equations): use whnf on recursive
 definition arguments

The idea is to expose "hidden" datatypes.
---
 src/library/definitional/equations.cpp |  2 ++
 tests/lean/run/eq25.lean               | 11 +++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/lean/run/eq25.lean

diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 1984ce2c0..20aa143b7 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -467,6 +467,8 @@ class equation_compiler_fn {
         for (expr const & fn : m_fns) {
             buffer<expr> args;
             expr r_type       = to_telescope(mlocal_type(fn), args);
+            for (expr & arg : args)
+                arg = update_mlocal(arg, whnf(mlocal_type(arg)));
             list<expr> ctx    = to_list(args);
             list<optional<name>> vstack = map2<optional<name>>(ctx, [](expr const & e) {
                     return optional<name>(mlocal_name(e));
diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean
new file mode 100644
index 000000000..823ac0e6d
--- /dev/null
+++ b/tests/lean/run/eq25.lean
@@ -0,0 +1,11 @@
+inductive N :=
+O : N,
+S : N → N
+
+definition Nat := N
+
+open N
+
+definition add : Nat → Nat → Nat,
+add O     b := b,
+add (S a) b := S (add a b)