Print Custom Notation

Stream: general

[Jeffrey Li]

Hi, I was wondering if there was a way for custom defined notation to appear in the Lean print messages? For example, if I have inner product defined

local notation `⟪`x`, `y`⟫` := @inner K V _ x y

when i print it, for example #check ⟪v,w⟫, it still results in inner v w. Is there a way for the printed result to be <<v, w >> instead? Thanks

[Yury G. Kudryashov]

Side note: should we get rid of all those local notations for inner? E.g., we can use ⟪x, y⟫ for real-valued inner product and ⟪x, y⟫_K for K-valued inner product.

[Gabriel Ebner]

@Jeffrey Li Yes, in general this just works. However the reason it doesn't work here is because of the @ in front. There is little we can do about it in Lean 3.

[Frédéric Dupuis]

Yury G. Kudryashov said:

Side note: should we get rid of all those local notations for inner? E.g., we can use ⟪x, y⟫ for real-valued inner product and ⟪x, y⟫_K for K-valued inner product.

To be honest, I don't really like the idea of reserving ⟪x, y⟫ for the real-valued inner product, I much prefer the current situation where we can define this to be the inner product over some arbitrary field at the top of the file.

[Joseph Myers]

And when you want the real inner product, it's better to use open_locale real_inner_product_space at the top of your file rather than doing your own local notation. (Likewise open_locale complex_inner_product_space.)