circumflex notation

Stream: general

[Miko de Amsterdamo]

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]

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

[Miko de Amsterdamo]

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

[Simon Hudon]

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

[Miko de Amsterdamo]

Thanks!