Merge branch 'master' into info-theory/entropy

Author: semaraugusto

Mathlib/Order/Notation.lean

@@ -113,27 +113,33 @@ private meta def hasLinearOrder (u : Level) (α : Q(Type u)) (cls : Q(Type u →
 
 /-- Delaborate `max x y` into `x ⊔ y` if the type is not a linear order. -/
 @[delab app.Max.max]
-meta def delabSup : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
-  let_expr f@Max.max α inst _ _ := ← getExpr | failure
-  have u := f.constLevels![0]!
-  if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
-    failure -- use the default delaborator
-  let x ← withNaryArg 2 delab
-  let y ← withNaryArg 3 delab
-  let stx ← `($x ⊔ $y)
-  annotateGoToSyntaxDef stx
+meta def delabSup : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 4 do
+    let_expr f@Max.max α inst _ _ := ← getExpr | failure
+    have u := f.constLevels![0]!
+    if ← hasLinearOrder u α q(Max) q($(linearOrderToMax u)) inst then
+      failure -- use the default delaborator
+    let x ← withNaryArg 2 delab
+    let y ← withNaryArg 3 delab
+    let stx ← `($x ⊔ $y)
+    annotateGoToSyntaxDef stx
 
 /-- Delaborate `min x y` into `x ⊓ y` if the type is not a linear order. -/
 @[delab app.Min.min]
-meta def delabInf : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation do
-  let_expr f@Min.min α inst _ _ := ← getExpr | failure
-  have u := f.constLevels![0]!
-  if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
-    failure -- use the default delaborator
-  let x ← withNaryArg 2 delab
-  let y ← withNaryArg 3 delab
-  let stx ← `($x ⊓ $y)
-  annotateGoToSyntaxDef stx
+meta def delabInf : Delab :=
+  whenNotPPOption getPPExplicit <|
+  whenPPOption getPPNotation <|
+  withOverApp 4 do
+    let_expr f@Min.min α inst _ _ := ← getExpr | failure
+    have u := f.constLevels![0]!
+    if ← hasLinearOrder u α q(Min) q($(linearOrderToMin u)) inst then
+      failure -- use the default delaborator
+    let x ← withNaryArg 2 delab
+    let y ← withNaryArg 3 delab
+    let stx ← `($x ⊓ $y)
+    annotateGoToSyntaxDef stx
 
 end Mathlib.Meta
 

MathlibTest/Delab/SupInf.lean

@@ -1,5 +1,5 @@
-import Mathlib
-
+module
+import Mathlib.Data.Real.Archimedean
 
 /-- info: max 1 2 : ℕ -/
 #guard_msgs in
@@ -82,3 +82,25 @@ set_option pp.explicit true in
 #check min (max a b) c
 
 end
+
+section Apply
+
+variable {ι α : Type*} [Lattice α] (f g : ι → α) (i : ι)
+
+/-- info: (f ⊔ g) i : α -/
+#guard_msgs in
+#check (f ⊔ g) i
+
+/-- info: (f ⊔ g) i : α -/
+#guard_msgs in
+#check max f g i
+
+/-- info: (f ⊓ g) i : α -/
+#guard_msgs in
+#check (f ⊓ g) i
+
+/-- info: (f ⊓ g) i : α -/
+#guard_msgs in
+#check min f g i
+
+end Apply

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1f22a4f44c1726b61fab3c2c75e0651f35c795dc",
+   "rev": "f0440aecee888582922e892d573b8726c09a1f6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",