how is field notation implemented?

Stream: general

[Asei Inoue]

How is field notation implemented in Lean? Are they macros as well as pipeline notation?

[Kyle Miller]

It's part of the app elaborator itself. Take a look at the match in docs#Lean.Elab.Term.elabAppFn

[Asei Inoue]

@Kyle Miller Thank you but the link is 404!

[Utensil Song]

You can find elabAppFn here: https://github.com/leanprover/lean4/blob/873ef2d894af80d8fc672e35f7e28bae314a1f6f/src/Lean/Elab/App.lean#L1344

It's a private def, so it's not shown in the docs.