Zulip Chat Archive

Stream: general

Topic: Print Custom Notation


Jeffrey Li (Dec 06 2021 at 22:19):

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 (Dec 07 2021 at 08:23):

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 (Dec 07 2021 at 09:54):

@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 (Dec 07 2021 at 16:21):

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 (Dec 08 2021 at 01:04):

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.)


Last updated: Dec 20 2023 at 11:08 UTC