Zulip Chat Archive

Stream: general

Topic: circumflex notation


view this post on Zulip Miko de Amsterdamo (Apr 12 2018 at 12:08):

What does this notation do? (hat/circumflex) I'm looking at an example in https://leanprover.github.io/programming_in_lean/#09_Writing_Automation.html and I found it in "(assume ha, h^.left ha)"

view this post on Zulip Simon Hudon (Apr 12 2018 at 12:16):

That's old notation. It was for field projection. Now it's only .

view this post on Zulip Miko de Amsterdamo (Apr 12 2018 at 12:17):

So the token ^. has been replaced by just . ?

view this post on Zulip Simon Hudon (Apr 12 2018 at 12:54):

That's correct. So . has the double duty of qualifying names with name spaces and resolving projections.

view this post on Zulip Miko de Amsterdamo (Apr 12 2018 at 12:54):

Thanks!


Last updated: May 08 2021 at 03:17 UTC