Notation for family of orderings

Stream: mathlib4

[Moritz R]

How does one get good notation in the output, when one has a family of orerings G -> PartialOrder F?
I currently have something alike:

import Mathlib.Data.Set.Defs
import Mathlib.Order.Defs.PartialOrder

class clWithOrder (F G : Type*) (order : outParam (G -> PartialOrder F))

abbrev clWithOrder.order [clWithOrder F G O] := O

set_option quotPrecheck false in
notation:50 a " <[" D:30 "] " b:50 => (clWithOrder.order D).lt a b

def usesOrder[clWithOrder F G O] (g : G) := { C : F | ∃ C', C' <[g] C}

/- prints with `<` instead of `<[D]`
def usesOrder.{u_1, u_2} : {F : Type u_1} →
  {G : Type u_2} → {O : G → PartialOrder F} → [clWithOrder F G O] → G → Set F :=
fun {F} {G} {O} [clWithOrder F G O] g => {C | ∃ C', C' < C}
-/
#print usesOrder

This has the issue, that it hides which ordering (i.e. which g) is used in the output, since it just uses <.

[Aaron Liu]

see also #metaprogramming / tactics > Delaborators for `IsOpen[t]` etc

[Moritz R]

So i should check in a custom delaborator wether my instance of lt comes from clWithOrder and if so, then pretty print it differently?

[Moritz R]

like this?

import Mathlib.Data.Set.Defs
import Mathlib.Order.Defs.PartialOrder
import Lean.PrettyPrinter.Delaborator

section bla

open Lean PrettyPrinter Delaborator SubExpr

class clWithOrder (F G : Type*) (order : outParam (G → PartialOrder F))

abbrev clWithOrder.order [clWithOrder F G O] := O

set_option quotPrecheck false in
notation:50 a " <[" D:30 "] " b:50 => (clWithOrder.order D).lt a b

-- Custom delaborator for LT.lt when used with clWithOrder
@[delab app.LT.lt]
def delabOrderLt : Delab := whenPPOption Lean.getPPNotation do
  let e ← getExpr
  guard <| e.isAppOfArity ``LT.lt 4
  -- Get the LT instance
  let ltInst := e.getArg! 1
  -- Check if it comes from clWithOrder.order
  if ltInst |>.getArg! 1 |>.getArg! 1 |>.isAppOf ``clWithOrder.order then
    let gExpr := ltInst.getArg! 1 |>.getArg! 1  |>.getArg! 4 -- Extract g
    let g ← delab gExpr
    let a ← withNaryArg 2 delab
    let b ← withNaryArg 3 delab
    `($a <[ $g ] $b)
  else
    failure

def usesOrder [clWithOrder F G O] (g : G) :=
  { C : F | ∃ C', C' <[g] C }

#print usesOrder  -- now shows <[g]

end bla

[Aaron Liu]

you might wanna also check if it changes delab of just regular lt expressions

[Moritz R]

Do you mean testing it, or putting some programmatical check that i don't know?

[Moritz R]

lemma zzz (a B : Nat) : a < b := by sorry
#print zzz

this still prints correctly

[Moritz R]

Is that what you mean?

[Aaron Liu]

yeah I mean just testing it

[Moritz R]

i have been getting some random Panics every few minutes, even while only staring at the screen.
I have now guarded all the indexes, which seems to work:

@[delab app.LT.lt]
meta def delabOrderLt : Delab := whenPPOption Lean.getPPNotation do
  let e ← getExpr
  guard <| e.isAppOfArity ``LT.lt 4
  -- Get the LT instance
  let ltInst := e.getArg! 1
  guard <| ltInst.getAppNumArgs ≥ 2
  let ltInst_arg1 := ltInst |>.getArg! 1
  guard <| ltInst_arg1.getAppNumArgs ≥ 2
  let ltInst_arg1_arg1 := ltInst_arg1 |>.getArg! 1
  guard <| ltInst_arg1_arg1.getAppNumArgs ≥ 6
  let ltInst_arg1_arg1_arg5 := ltInst_arg1_arg1 |>.getArg! 5
  -- Check if it comes from clWithOrder.order
  if ltInst_arg1_arg1 |>.isAppOf ``clWithOrder.order.order then
    let gExpr := ltInst_arg1_arg1_arg5 -- Extract g
    let g ← delab gExpr
    let a ← withNaryArg 2 delab
    let b ← withNaryArg 3 delab
    `($a <[ $g ] $b)
  else
    failure