From a450ad5a95e9c704e1cd42e4293755c61226b09e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Jul 2014 11:24:01 -0700
Subject: [PATCH] feat(frontends/lean/inductive_cmd): improve notation for
 declaring 'empty' inductive datatypes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/hott/logic.lean              |  3 +--
 library/standard/logic.lean          |  3 +--
 src/frontends/lean/inductive_cmd.cpp | 18 +++++++++++++-----
 3 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/library/hott/logic.lean b/library/hott/logic.lean
index 9a6cf85a3..5b263f374 100644
--- a/library/hott/logic.lean
+++ b/library/hott/logic.lean
@@ -152,8 +152,7 @@ notation `Ω` `(` A `,` a `)` := loop_space A a
 definition loop2d_space (A : Type) (a : A) := (refl a) = (refl a)
 notation `Ω²` `(` A `,` a `)` := loop2d_space A a
 
-inductive empty : Type :=
--- empty
+inductive empty : Type
 
 theorem empty_elim (c : Type) (H : empty) : c
 := empty_rec (λ e, c) H
diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index 3a05aa8b7..f15aa99d9 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -3,8 +3,7 @@
 -- Authors: Leonardo de Moura, Jeremy Avigad
 definition Prop [inline] := Type.{0}
 
-inductive false : Prop :=
--- No constructors
+inductive false : Prop
 
 theorem false_elim (c : Prop) (H : false) : c
 := false_rec c H
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index bede699f3..955bbbf9c 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -279,17 +279,25 @@ struct inductive_cmd_fn {
             name d_name = parse_decl_name();
             parse_inductive_univ_params();
             expr d_type = parse_datatype_type();
-            m_p.check_token_next(g_assign, "invalid inductive declaration, ':=' expected");
+            bool empty_type = true;
+            if (m_p.curr_is_token(g_assign)) {
+                empty_type = false;
+                m_p.next();
+            }
             level_param_names d_lvls;
             std::tie(d_type, d_lvls) = elaborate_inductive_type(d_type);
             if (!m_first) {
                 check_params(d_type, *first_d_type);
                 check_levels(d_lvls, *first_d_lvls);
             }
-            buffer<expr> params;
-            add_params_to_local_scope(d_type, params);
-            auto d_intro_rules = parse_intro_rules(params);
-            decls.push_back(inductive_decl(d_name, d_type, d_intro_rules));
+            if (empty_type) {
+                decls.push_back(inductive_decl(d_name, d_type, list<intro_rule>()));
+            } else {
+                buffer<expr> params;
+                add_params_to_local_scope(d_type, params);
+                auto d_intro_rules = parse_intro_rules(params);
+                decls.push_back(inductive_decl(d_name, d_type, d_intro_rules));
+            }
             if (!m_p.curr_is_token(g_with)) {
                 m_levels.append(m_explict_levels);
                 for (auto l : d_lvls) m_levels.push_back(l);