cleanup

This PR causes structure instance notation to be tagged with the
constructor when `pp.tagAppFns` is true. This will make docgen will have
`{` and `}` be links to the structure constructor.

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -20,15 +20,25 @@ open TSyntax.Compat
 /--
 If `cond` is true, wraps the syntax produced by `d` in a type ascription.
 -/
-def withTypeAscription (d : Delab) (cond : Bool := true) : DelabM Term := do
+def withTypeAscription (d : Delab) (cond : Bool := true) : Delab := do
   let stx ← d
   if cond then
-    let stx ← annotateCurPos stx
+    let stx ← annotateTermInfoUnlessAnnotated stx
     let typeStx ← withType delab
     `(($stx : $typeStx))
   else
     return stx
 
+/--
+If `pp.tagAppFns` is set, then `d` is evaluated with the delaborated head constant as the ref.
+-/
+def withFnRefWhenTagAppFns (d : Delab) : Delab := do
+  if (← getExpr).getAppFn.isConst && (← getPPOption getPPTagAppFns) then
+    let head ← withNaryFn delab
+    withRef head <| d
+  else
+    d
+
 /--
 Wraps the identifier (or identifier with explicit universe levels) with `@` if `pp.analysis.blockImplicit` is set to true.
 -/
@@ -637,7 +647,7 @@ def delabStructureInstance : Delab := do
         else
           return (i + 1, args))
     withTypeAscription (cond := (← withType <| getPPOption getPPStructureInstanceType)) do
-      `(⟨$[$args],*⟩)
+      withFnRefWhenTagAppFns `(⟨$[$args],*⟩)
   else
     /-
     Otherwise, we use structure instance notation.
@@ -650,7 +660,7 @@ def delabStructureInstance : Delab := do
     let (_, fields) ← collectStructFields s.induct levels params #[] {} s
     let tyStx? : Option Term ← withType do
       if ← getPPOption getPPStructureInstanceType then delab else pure none
-    `({ $fields,* $[: $tyStx?]? })
+    withFnRefWhenTagAppFns `({ $fields,* $[: $tyStx?]? })
 
 
 /-- State for `delabAppMatch` and helpers. -/

tests/lean/grind/decide.lean

@@ -0,0 +1,21 @@
+---
+
+example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind
+
+---
+
+@[grind] theorem eq_head_or_mem_tail_of_mem_cons {a b : α} {l : List α} :
+    a ∈ b :: l → a = b ∨ a ∈ l := List.mem_cons.mp
+
+attribute [grind] List.mem_cons_self, List.mem_cons_of_mem
+
+-- This succeeds:
+example [DecidableEq α] {l : List α} :
+    (y ∈ a :: l) = (y = a) ∨ y ∈ l := by
+  grind
+
+
+-- but inserting some `decide`s fails:
+example [BEq α] [LawfulBEq α] {l : List α} :
+    decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
+  grind

tests/lean/grind/list_problems.lean

@@ -1,6 +1,32 @@
+reset_grind_attrs%
+
+attribute [grind] List.length_set
+attribute [grind →] List.eq_nil_of_length_eq_zero
+
+open List in
+example {as : List α} {i : Nat} (h : i < as.length) :
+    as.set i as[i] = as := by
+  apply ext_getElem
+  · sorry
+  · -- works:
+    grind [getElem_set]
+
+attribute [grind] List.getElem_set
+
+open List in
+example {as : List α} {i : Nat} (h : i < as.length) :
+    as.set i as[i] = as := by
+  apply ext_getElem
+  · sorry
+  · -- fails:
+    grind
+
+---
+reset_grind_attrs%
+
 theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a := by
   induction l
-  · grind
+  · sorry
   · cases i
     · -- Better support for implication and dependent implication.
       -- We need inequality propagation (or case-splits)
@@ -8,9 +34,14 @@ theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.le
     · -- Similarly
       grind
 
+---
+reset_grind_attrs%
+
 attribute [grind] List.getElem_append_left List.getElem_append_right
 attribute [grind] List.length_cons List.length_nil
 
 example {l : List α} {a : α} {i : Nat} (h : i = l.length) (w) :
     (l ++ [a])[i]'w = a := by
   grind -- Similar to issue above.
+
+---