chore: pp.proofs.withType is now false by default (#3379)

`pp.proofs.withType := true` often produces too much noise in the info
view.

RELEASES.md

@@ -16,6 +16,8 @@ v4.7.0 (development in progress)
   The `pp.proofs.threshold` option lets small proofs always be pretty printed.
   [#3241](https://github.com/leanprover/lean4/pull/3241).
 
+* `pp.proofs.withType` is now set to false by default to reduce noise in the info view.
+
 v4.6.0
 ---------
 

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -121,7 +121,7 @@ register_builtin_option pp.proofs : Bool := {
   descr    := "(pretty printer) display proofs when true, and replace proofs appearing within expressions by `⋯` when false"
 }
 register_builtin_option pp.proofs.withType : Bool := {
-  defValue := true
+  defValue := false
   group    := "pp"
   descr    := "(pretty printer) when `pp.proofs` is false, adds a type ascription to the omitted proof"
 }

tests/lean/1074a.lean.expected.out

@@ -1,4 +1,4 @@
 Brx.interp._eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
   Brx.interp H_2 =
-    match (⋯ : True ∧ Brx z) with
-    | (⋯ : True ∧ Brx z) => Brx.interp Hz
+    match ⋯ with
+    | ⋯ => Brx.interp Hz

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 := (⋯ : 0 < Nat.succ n) } v = insert a { val := 0, isLt := (⋯ : 0 < Nat.succ n) } v : Prop
+  insert a { val := 0, isLt := ⋯ } v = insert a { val := 0, isLt := ⋯ } v : Prop
 but is expected to have type
-  insert a { val := 0, isLt := (⋯ : 0 < Nat.succ n) } v = cons a v : Prop
+  insert a { val := 0, isLt := ⋯ } v = cons a v : Prop

tests/lean/1856.lean.expected.out

@@ -6,4 +6,4 @@ i : α
 β : α → Type ?u
 f : (j : α) → β j
 x : α
-⊢ (if h : x = i then (⋯ : i = x) ▸ f i else f x) = f x
+⊢ (if h : x = i then ⋯ ▸ f i else f x) = f x

tests/lean/986.lean.expected.out

@@ -3,8 +3,7 @@ Array.insertionSort.swapLoop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Boo
 Array.insertionSort.swapLoop._eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
   (h : Nat.succ j' < Array.size a) :
   Array.insertionSort.swapLoop lt a (Nat.succ j') h =
-    let_fun h' := (⋯ : j' < Array.size a);
+    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'
-        (⋯ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
+      Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
     else a

tests/lean/congrThm.lean.expected.out

@@ -1,8 +1,6 @@
 ∀ (p p_1 : Prop),
   p = p_1 →
-    ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat) (e_a : a = a_1) (h : a > 0),
-      g p a h = g p_1 a_1 (⋯ : a_1 > 0)
+    ∀ {inst : Decidable p} {inst_1 : Decidable p_1} (a a_1 : Nat) (e_a : a = a_1) (h : a > 0), g p a h = g p_1 a_1 ⋯
 ∀ (p p_1 : Prop),
   p = p_1 →
-    ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat) (e_a : a = a_1) (h : a > 0),
-      g p a h = g p_1 a_1 (⋯ : a_1 > 0)
+    ∀ {inst : Decidable p} [inst_1 : Decidable p_1] (a a_1 : Nat) (e_a : a = a_1) (h : a > 0), g p a h = g p_1 a_1 ⋯

tests/lean/congrThmIssue.lean.expected.out

@@ -4,10 +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 := (⋯ : i < cap) }) = true
+h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing { val := i, isLt := ⋯ }) = true
 i : Nat
 h : i < size
-⊢ Option.isSome
-      (if h_1 : i < cap then backing { val := i, isLt := (⋯ : { val := i, isLt := (⋯ : i < cap + cap) }.val < cap) }
-      else none) =
-    true
+⊢ Option.isSome (if h_1 : i < cap then backing { val := i, isLt := ⋯ } else none) = true

tests/lean/diamond9.lean.expected.out

@@ -1,2 +1,2 @@
 constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R
-Ring.mk (fun x n => Int.toNat x * n) (⋯ : ∀ (a : Nat), 0 * a = 0) : Ring Nat
+Ring.mk (fun x n => Int.toNat x * n) ⋯ : Ring Nat

tests/lean/heapSort.lean.expected.out

@@ -13,5 +13,5 @@ Array.heapSort.loop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : B
     match e : BinaryHeap.max a with
     | none => out
     | some x =>
-      let_fun this := (⋯ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a);
+      let_fun this := ⋯;
       Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)

tests/lean/letFun.lean.expected.out

@@ -15,7 +15,7 @@ a b : Nat
 h : a > b
 ⊢ b < a
 let_fun n := 5;
-{ val := [], property := (⋯ : 0 ≤ n) } : { as // List.length as ≤ 5 }
+{ val := [], property := ⋯ } : { as // List.length as ≤ 5 }
 rfl : (let_fun n := 5;
   n) =
   let_fun n := 5;

tests/lean/match1.lean.expected.out

@@ -11,9 +11,9 @@
 ---- inv
 10
 match1.lean:82:0-82:73: error: dependent elimination failed, type mismatch when solving alternative with type
-  motive 0 (Vec.cons head✝ Vec.nil) (⋯ : VecPred P (Vec.cons head✝ Vec.nil))
+  motive 0 (Vec.cons head✝ Vec.nil) ⋯
 but expected
-  motive x✝ (Vec.cons head✝ tail✝) (⋯ : VecPred P (Vec.cons head✝ tail✝))
+  motive x✝ (Vec.cons head✝ tail✝) ⋯
 [false, true, true]
 match1.lean:119:0-119:41: error: dependent match elimination failed, inaccessible pattern found
   .(j + j)

tests/lean/ppProofs.lean.expected.out

@@ -11,13 +11,13 @@ context:
 b : β
 a : α
 h : α = β
-⊢ (⋯ : α = β) ▸ a = b
+⊢ ⋯ ▸ a = b
 ppProofs.lean:10:50-10:98: error: unsolved goals
 α β : Sort ?u
 b : β
 a : α
 h : α = β
-⊢ (⋯ : α = β) ▸ a = b
+⊢ ⋯ ▸ a = b
 ppProofs.lean:12:50-12:51: error: don't know how to synthesize placeholder
 context:
 α β : Sort u_1
@@ -32,7 +32,7 @@ b : β
 a : α
 h : α = β
 ⊢ id h ▸ a = b
-let x := (⋯ : 1 ≤ Nat.succ 1);
+let x := ⋯;
 0 : Nat
 let x := Nat.le_succ 1;
 0 : Nat

tests/lean/run/PPTopDownAnalyze.lean

@@ -264,6 +264,7 @@ The `#testDelab` expects it can elaborate the expression, so here is a macro rul
 local macro_rules | `(⋯) => `(_)
 
 set_option pp.proofs false in
+set_option pp.proofs.withType true in
 #testDelab @NeedsAnalysis.mk Unit
   expecting (⋯ : NeedsAnalysis (α := Unit))
 

tests/lean/wfrecUnusedLet.lean.expected.out

@@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
-    2 * a (n - 1) (⋯ : (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n - 1) n)
+    2 * a (n - 1) ⋯