From e3249dfdb9f1cecda541eb2d2230fd5c957a273d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 May 2017 13:36:58 -0700
Subject: [PATCH] test(tests/lean/run/term_app): add test for nested inductive
 type

---
 tests/lean/run/term_app.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 tests/lean/run/term_app.lean

diff --git a/tests/lean/run/term_app.lean b/tests/lean/run/term_app.lean
new file mode 100644
index 0000000000..c0088319f5
--- /dev/null
+++ b/tests/lean/run/term_app.lean
@@ -0,0 +1,14 @@
+inductive term
+| const : string → term
+| app   : string → list term → term
+
+/- TODO(Leo): remove after we fix bug in lemma generator. -/
+set_option eqn_compiler.lemmas false
+
+mutual def num_consts, num_consts_lst
+with num_consts : term → nat
+| (term.const n)  := 1
+| (term.app n ts) := num_consts_lst ts
+with num_consts_lst : list term → nat
+| []      := 0
+| (t::ts) := num_consts t + num_consts_lst ts