From a6dc9e4ef3edb6956dfeb4b61ef6a532ed3d836d Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 17 May 2021 16:13:27 -0400
Subject: [PATCH] feat: `class abbrev` now supports a type spec (+ test)

---
 src/Init/NotationExtra.lean     |  8 ++++----
 tests/lean/run/classAbbrev.lean | 11 +++++++++++
 2 files changed, 15 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/classAbbrev.lean

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 0f886cb8d3..9c1a8d5e58 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -139,14 +139,14 @@ macro_rules
   attribute [instance] C.mk
   ```
 -/
-syntax declModifiers "class " "abbrev " declId 
-  bracketedBinder* ":=" withPosition(group(colGe term ","?)*) : command
+syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)? 
+  ":=" withPosition(group(colGe term ","?)*) : command
 
 macro_rules
-  | `($mods:declModifiers class abbrev $id $params* := $[ $parents:term $[,]? ]*) =>
+  | `($mods:declModifiers class abbrev $id $params* $[: $ty:term]? := $[ $parents:term $[,]? ]*) =>
     let name := id[0]
     let ctor := mkIdentFrom name <| name.getId.modifyBase (. ++ `mk)
-    `($mods:declModifiers class $id $params* extends $[$parents:term],*
+    `($mods:declModifiers class $id $params* extends $[$parents:term],* $[: $ty]?
       attribute [instance] $ctor)
 
 /-
diff --git a/tests/lean/run/classAbbrev.lean b/tests/lean/run/classAbbrev.lean
new file mode 100644
index 0000000000..6e209b8222
--- /dev/null
+++ b/tests/lean/run/classAbbrev.lean
@@ -0,0 +1,11 @@
+class Refl.{U} {α : Type U} (R : α → α → Prop) : Prop :=
+  refl (a : α) : R a a
+
+class Symm.{U} {α : Type U} (R : α → α → Prop) : Prop :=
+  symm {a b : α} : R a b → R b a
+
+/--
+  An example decl modifier (a doc comment).
+-/
+class abbrev PEquiv.{U} {α : Type U} (R : α → α → Prop) : Prop 
+  := Refl R, Symm R