Notation unfolding in infoview

Stream: lean4

[Horatiu Cheval]

In the following example, the notation for Formula.knows gets unfolded in the infoview when doing #check 𝕂 φ.
Can I make it so that the notation is preserved in the infoview, just like the prefix below for Formula.negation?
Or more generally, is there some customizability regarding what happens with notations when they are printed?

inductive Formula
| negation : Formula → Formula
| knows : Formula → Formula

prefix:90 "∼" => Formula.negation
notation "𝕂" => Formula.knows

variable (φ : Formula)

#check ∼φ
-- ∼φ : Formula
#check 𝕂 φ
-- Formula.knows φ : Formula

[Alexander Bentkamp]

You can use an Unexpander:

@[appUnexpander Formula.knows]
def unexpandKnows : Lean.PrettyPrinter.Unexpander
| `(Formula.knows $x) => `(𝕂 $x)
| _ => throw ()