Topic: circumflex notation
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)"
Simon Hudon (Apr 12 2018 at 12:16):
That's old notation. It was for field projection. Now it's only
Miko de Amsterdamo (Apr 12 2018 at 12:17):
So the token
^. has been replaced by just
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.
Miko de Amsterdamo (Apr 12 2018 at 12:54):
Last updated: May 08 2021 at 03:17 UTC