From 4ad7e709aab17d2029e002b5816285e615a4674c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Aug 2014 07:52:20 -0700 Subject: [PATCH] feat(frontends/lean): default for inductive types, closes #32 Signed-off-by: Leonardo de Moura --- src/frontends/lean/inductive_cmd.cpp | 12 +++++++++--- tests/lean/run/indimp.lean | 21 +++++++++++++++++++++ 2 files changed, 30 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/indimp.lean diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 2e815b865..75986c56d 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -136,10 +136,16 @@ struct inductive_cmd_fn { expr type; buffer ps; m_pos = m_p.pos(); - if (!m_p.curr_is_token(g_colon)) { + if (m_p.curr_is_token(g_assign)) { + type = mk_sort(mk_level_placeholder()); + } else if (!m_p.curr_is_token(g_colon)) { m_p.parse_binders(ps); - m_p.check_token_next(g_colon, "invalid inductive declaration, ':' expected"); - type = m_p.parse_scoped_expr(ps); + if (m_p.curr_is_token(g_colon)) { + m_p.next(); + type = m_p.parse_scoped_expr(ps); + } else { + type = mk_sort(mk_level_placeholder()); + } type = Pi(ps, type, m_p); } else { m_p.next(); diff --git a/tests/lean/run/indimp.lean b/tests/lean/run/indimp.lean new file mode 100644 index 000000000..bb3a24499 --- /dev/null +++ b/tests/lean/run/indimp.lean @@ -0,0 +1,21 @@ +abbreviation Prop := Type.{0} + +inductive nat := +| zero : nat +| succ : nat → nat + +inductive list (A : Type) := +| nil {} : list A +| cons : A → list A → list A + +inductive list2 (A : Type) : Type := +| nil2 {} : list2 A +| cons2 : A → list2 A → list2 A + +inductive and (A B : Prop) : Prop := +| and_intro : A → B → and A B + +inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) := +| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f + +