feat(frontends/lean/inductive_cmd): notation for enumeration types

src/frontends/lean/inductive_cmd.cpp

@@ -263,9 +263,14 @@ struct inductive_cmd_fn {
                 m_p.check_token_next(get_rparen_tk(), "invalid introduction rule, ')' expected");
                 m_implicit_infer_map.insert(intro_name, implicit_infer_kind::None);
             }
-            m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
+            if (!m_params.empty() || m_p.curr_is_token(get_colon_tk())) {
-            expr intro_type = m_p.parse_expr();
+                m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
-            intros.push_back(intro_rule(intro_name, intro_type));
+                expr intro_type = m_p.parse_expr();
+                intros.push_back(intro_rule(intro_name, intro_type));
+            } else {
+                expr intro_type = mk_constant(ind_name);
+                intros.push_back(intro_rule(intro_name, intro_type));
+            }
             if (!m_p.curr_is_token(get_comma_tk()))
                 break;
             m_p.next();

tests/lean/run/enum.lean

@@ -0,0 +1,16 @@
+import logic
+
+inductive Three :=
+zero : Three,
+one  : Three,
+two  : Three
+
+namespace Three
+
+  theorem disj (a : Three) : a = zero ∨ a = one ∨ a = two :=
+  rec (or.inl rfl) (or.inr (or.inl rfl)) (or.inr (or.inr rfl)) a
+
+  theorem example (a : Three) : a ≠ zero → a ≠ one → a = two :=
+  rec (λ h₁ h₂, absurd rfl h₁) (λ h₁ h₂, absurd rfl h₂) (λ h₁ h₂, rfl) a
+
+end Three