From 3bb3efdedc7bb88e5897605d180ff04bb3b5f9b8 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 12 Sep 2022 20:14:16 -0400
Subject: [PATCH] feat: allow optional type in `example`

---
 src/Lean/Elab/DefView.lean       | 4 ++--
 src/Lean/Parser/Command.lean     | 2 +-
 tests/lean/331.lean              | 3 ++-
 tests/lean/331.lean.expected.out | 2 ++
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index f89755c074..4713f17711 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -137,11 +137,11 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
 
 def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "example " >> declSig >> declVal
-  let (binders, type) := expandDeclSig stx[1]
+  let (binders, type) := expandOptDeclSig stx[1]
   let id              := mkIdentFrom stx `_example
   let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
   { ref := stx, kind := DefKind.example, modifiers := modifiers,
-    declId := declId, binders := binders, type? := some type, value := stx[2] }
+    declId := declId, binders := binders, type? := type, value := stx[2] }
 
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index c636250270..4d13a5ada2 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -76,7 +76,7 @@ def «opaque»         := leading_parser "opaque " >> declId >> ppIndent declSig
 def «instance»       := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
 def «axiom»          := leading_parser "axiom " >> declId >> ppIndent declSig
 /- As `declSig` starts with a space, "example" does not need a trailing space. -/
-def «example»        := leading_parser "example" >> ppIndent declSig >> declVal
+def «example»        := leading_parser "example" >> ppIndent optDeclSig >> declVal
 def ctor             := leading_parser "\n| " >> ppIndent (declModifiers true >> rawIdent >> optDeclSig)
 def derivingClasses  := sepBy1 (group (ident >> optional (" with " >> Term.structInst))) ", "
 def optDeriving      := leading_parser optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
diff --git a/tests/lean/331.lean b/tests/lean/331.lean
index a35c1d53bc..c3d13b8e99 100644
--- a/tests/lean/331.lean
+++ b/tests/lean/331.lean
@@ -2,5 +2,6 @@ structure Foo where
   foo : Nat
 
 def baz {x : _} := Foo.mk x -- works fine
-
+example {x : _} := Foo.mk x
 def qux {x : _} : Foo := Foo.mk x
+example {x : _} : Foo := Foo.mk x
diff --git a/tests/lean/331.lean.expected.out b/tests/lean/331.lean.expected.out
index 5728502d1c..70a9adb0e5 100644
--- a/tests/lean/331.lean.expected.out
+++ b/tests/lean/331.lean.expected.out
@@ -1,2 +1,4 @@
 331.lean:6:13-6:14: error: failed to infer binder type
 when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
+331.lean:7:13-7:14: error: failed to infer binder type
+when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed