From fba9c038129c44189919e08f821204880efbb32b Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 9 Mar 2024 09:05:48 -0800
Subject: [PATCH] feat: apply `pp_using_anonymous_constructor` attribute

This attribute is applied to the following structures: `Sigma`, `PSigma`, `PProd`, `And`, `Subtype`, and `Fin`.
These were given this attribute in Lean 3.
---
 RELEASES.md                                     |  1 +
 src/Init/Core.lean                              |  2 ++
 src/Init/Prelude.lean                           |  4 ++++
 tests/lean/1081.lean.expected.out               |  4 ++--
 tests/lean/243.lean.expected.out                |  4 ++--
 tests/lean/congrThmIssue.lean.expected.out      |  4 ++--
 tests/lean/decreasing_by.lean.expected.out      | 15 +++++----------
 tests/lean/issue2981.lean.expected.out          |  4 +---
 tests/lean/letFun.lean.expected.out             |  2 +-
 tests/lean/run/986.lean                         |  3 +--
 tests/lean/run/PPTopDownAnalyze.lean            |  4 ++--
 tests/lean/run/funind_tests.lean                |  2 +-
 tests/lean/run/litToCtor.lean                   |  6 +++---
 tests/lean/run/ppUsingAnonymousConstructor.lean | 12 ++++++++++++
 14 files changed, 39 insertions(+), 28 deletions(-)

diff --git a/RELEASES.md b/RELEASES.md
index 761006221357..97c044f0c69a 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -55,6 +55,7 @@ v4.8.0 (development in progress)
 
 * Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
   rather than `{a := x, b := y, c := z}`.
+  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
 
 Breaking changes:
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index d27672e92788..09e305af3409 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -165,6 +165,7 @@ whose first component is `a : α` and whose second component is `b : β a`
 It is sometimes known as the dependent sum type, since it is the type level version
 of an indexed summation.
 -/
+@[pp_using_anonymous_constructor]
 structure Sigma {α : Type u} (β : α → Type v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : Sigma β`.
   (This will usually require a type ascription to determine `β`
@@ -190,6 +191,7 @@ which can cause problems for universe level unification,
 because the equation `max 1 u v = ?u + 1` has no solution in level arithmetic.
 `PSigma` is usually only used in automation that constructs pairs of arbitrary types.
 -/
+@[pp_using_anonymous_constructor]
 structure PSigma {α : Sort u} (β : α → Sort v) where
   /-- Constructor for a dependent pair. If `a : α` and `b : β a` then `⟨a, b⟩ : PSigma β`.
   (This will usually require a type ascription to determine `β`
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 23d746844386..c7132e7b3b35 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -488,6 +488,7 @@ attribute [unbox] Prod
 Similar to `Prod`, but `α` and `β` can be propositions.
 We use this type internally to automatically generate the `brecOn` recursor.
 -/
+@[pp_using_anonymous_constructor]
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
   fst : α
@@ -509,6 +510,7 @@ structure MProd (α β : Type u) where
 constructed and destructed like a pair: if `ha : a` and `hb : b` then
 `⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.
 -/
+@[pp_using_anonymous_constructor]
 structure And (a b : Prop) : Prop where
   /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
   intro ::
@@ -575,6 +577,7 @@ a pair-like type, so if you have `x : α` and `h : p x` then
 `⟨x, h⟩ : {x // p x}`. An element `s : {x // p x}` will coerce to `α` but
 you can also make it explicit using `s.1` or `s.val`.
 -/
+@[pp_using_anonymous_constructor]
 structure Subtype {α : Sort u} (p : α → Prop) where
   /-- If `s : {x // p x}` then `s.val : α` is the underlying element in the base
   type. You can also write this as `s.1`, or simply as `s` when the type is
@@ -1809,6 +1812,7 @@ theorem System.Platform.numBits_eq : Or (Eq numBits 32) (Eq numBits 64) :=
 `Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.
 It is the "canonical type with `n` elements".
 -/
+@[pp_using_anonymous_constructor]
 structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.val : ℕ` is the described number. It can also be
   written as `i.1` or just `i` when the target type is known. -/
diff --git a/tests/lean/1081.lean.expected.out b/tests/lean/1081.lean.expected.out
index c2d58d1376fb..da51d3223c59 100644
--- a/tests/lean/1081.lean.expected.out
+++ b/tests/lean/1081.lean.expected.out
@@ -7,6 +7,6 @@ but is expected to have type
 1081.lean:23:4-23:7: error: type mismatch
   rfl
 has type
-  insert a { val := 0, isLt := ⋯ } v = insert a { val := 0, isLt := ⋯ } v : Prop
+  insert a ⟨0, ⋯⟩ v = insert a ⟨0, ⋯⟩ v : Prop
 but is expected to have type
-  insert a { val := 0, isLt := ⋯ } v = cons a v : Prop
+  insert a ⟨0, ⋯⟩ v = cons a v : Prop
diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out
index 86368e12cf79..39077e6323f7 100644
--- a/tests/lean/243.lean.expected.out
+++ b/tests/lean/243.lean.expected.out
@@ -1,5 +1,5 @@
 243.lean:2:10-2:14: error: application type mismatch
-  { fst := Bool, snd := true }
+  ⟨Bool, true⟩
 argument
   true
 has type
@@ -7,7 +7,7 @@ has type
 but is expected to have type
   Bool : Type
 243.lean:13:7-13:8: error: application type mismatch
-  { fst := A, snd := a }
+  ⟨A, a⟩
 argument
   a
 has type
diff --git a/tests/lean/congrThmIssue.lean.expected.out b/tests/lean/congrThmIssue.lean.expected.out
index 703ae545b5f7..4233da007e03 100644
--- a/tests/lean/congrThmIssue.lean.expected.out
+++ b/tests/lean/congrThmIssue.lean.expected.out
@@ -4,7 +4,7 @@ cap : Nat
 backing : Fin cap → Option α
 size : Nat
 h_size : size ≤ cap
-h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing { val := i, isLt := ⋯ }) = true
+h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing ⟨i, ⋯⟩) = true
 i : Nat
 h : i < size
-⊢ Option.isSome (if h_1 : i < cap then backing { val := i, isLt := ⋯ } else none) = true
+⊢ Option.isSome (if h_1 : i < cap then backing ⟨i, ⋯⟩ else none) = true
diff --git a/tests/lean/decreasing_by.lean.expected.out b/tests/lean/decreasing_by.lean.expected.out
index 9fbed680150f..0393f3755691 100644
--- a/tests/lean/decreasing_by.lean.expected.out
+++ b/tests/lean/decreasing_by.lean.expected.out
@@ -15,21 +15,17 @@ Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
 decreasing_by.lean:81:0-81:13: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
-    { fst := n, snd := dec2 m } { fst := n, snd := m }
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
-    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:91:0-91:22: error: unsolved goals
 case a
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
-    { fst := n, snd := dec2 m } { fst := n, snd := m }
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩
 
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
-    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
@@ -39,8 +35,7 @@ The arguments relate at each recursive call as follows:
 Please use `termination_by` to specify a decreasing measure.
 decreasing_by.lean:110:0-113:17: error: unsolved goals
 n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1
-    { fst := dec1 n, snd := 100 } { fst := n, snd := m }
+⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩
 decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 7e97fdc5c2b6..8b4e6c591169 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -8,6 +8,4 @@ Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ sizeOf n < sizeOf (Nat.succ n)
-n m : Nat
-⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 { fst := n, snd := m + 1 }
-    { fst := Nat.succ n, snd := m }
+n m : Nat ⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 ⟨n, m + 1⟩ ⟨Nat.succ n, m⟩
diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out
index c34bf215cee4..04855d77fe15 100644
--- a/tests/lean/letFun.lean.expected.out
+++ b/tests/lean/letFun.lean.expected.out
@@ -15,7 +15,7 @@ a b : Nat
 h : a > b
 ⊢ b < a
 let_fun n := 5;
-{ val := [], property := ⋯ } : { as // List.length as ≤ 5 }
+⟨[], ⋯⟩ : { as // List.length as ≤ 5 }
 rfl : (let_fun n := 5;
   n) =
   let_fun n := 5;
diff --git a/tests/lean/run/986.lean b/tests/lean/run/986.lean
index 1d7dc33fe1b8..a04427305a2c 100644
--- a/tests/lean/run/986.lean
+++ b/tests/lean/run/986.lean
@@ -12,8 +12,7 @@ info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α 
   (h : Nat.succ j' < Array.size a) :
   Array.insertionSort.swapLoop lt a (Nat.succ j') h =
     let_fun h' := ⋯;
-    if lt a[Nat.succ j'] a[j'] = true then
-      Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
+    if lt a[Nat.succ j'] a[j'] = true then Array.insertionSort.swapLoop lt (Array.swap a ⟨Nat.succ j', h⟩ ⟨j', h'⟩) j' ⋯
     else a
 -/
 #guard_msgs in
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 0a1c490902ff..dea11210e326 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -196,7 +196,7 @@ set_option pp.analyze.trustSubst true in
 
 set_option pp.analyze.trustId true in
 #testDelab Sigma.mk (β := fun α => α) Bool true
-  expecting { fst := _, snd := true }
+  expecting ⟨_, true⟩
 
 set_option pp.analyze.trustId false in
 #testDelab Sigma.mk (β := fun α => α) Bool true
@@ -330,7 +330,7 @@ set_option pp.analyze.explicitHoles false in
 
 set_option pp.analyze.trustSubtypeMk true in
 #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
-  expecting fun n val property => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
+  expecting fun n val property => List.length (⟨val, property⟩ : { x : List Nat // List.length x = n }).val = n
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 3e82eb99cf0e..7a1965c7d38e 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -721,7 +721,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
   (case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2)
   (case5 :
     ∀ (n m k : Nat) (x : Fin (k + 2)),
-      motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) :
+      motive n m (k + 1) ⟨0, ⋯⟩ → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) :
   ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
 -/
 #guard_msgs in
diff --git a/tests/lean/run/litToCtor.lean b/tests/lean/run/litToCtor.lean
index 0686262876bb..2d4c2301bf52 100644
--- a/tests/lean/run/litToCtor.lean
+++ b/tests/lean/run/litToCtor.lean
@@ -42,17 +42,17 @@ info: Int.ofNat 3
 #guard_msgs in
 #eval test (3 : Int)
 /--
-info: { val := 3, isLt := ⋯ }
+info: ⟨3, ⋯⟩
 -/
 #guard_msgs in
 #eval test (3 : Fin 5)
 /--
-info: { val := 0, isLt := ⋯ }
+info: ⟨0, ⋯⟩
 -/
 #guard_msgs in
 #eval test (0 : Fin 5)
 /--
-info: { val := 1, isLt := ⋯ }
+info: ⟨1, ⋯⟩
 -/
 #guard_msgs in
 #eval test (6 : Fin 5)
diff --git a/tests/lean/run/ppUsingAnonymousConstructor.lean b/tests/lean/run/ppUsingAnonymousConstructor.lean
index 22010d2d7c31..3d27b35fe59f 100644
--- a/tests/lean/run/ppUsingAnonymousConstructor.lean
+++ b/tests/lean/run/ppUsingAnonymousConstructor.lean
@@ -15,3 +15,15 @@ structure S where
 attribute [pp_using_anonymous_constructor] S
 /-- info: ⟨1, 2⟩ : S -/
 #guard_msgs in #check {x := 1, y := 2 : S}
+
+/-!
+`Fin`
+-/
+/-- info: ⟨2, ⋯⟩ : Fin 3 -/
+#guard_msgs in #check Fin.mk 2 (by omega : 2 < 3)
+
+/-!
+`Subtype`
+-/
+/-- info: ⟨2, ⋯⟩ : { n // n < 3 } -/
+#guard_msgs in #check (⟨2, by omega⟩ : {n : Nat // n < 3})