Struct projector

Stream: new members

[Patrick Johnson]

How exactly are field accessors defined in terms of rec? For instance, in this snippet:

structure A := (x : ℕ)
#print A.x

It prints

@[reducible]
def A.x : A → ℕ :=
λ (self : A), [A.x self]

I guess this is some pretty-printer artifact. First, I don't understand the square brackets there (obviously they don't represent a singleton list). Second, how can the function being defined reference itself? I was expecting to see a use of A.rec instead.

[Alex J. Best]

On mobile so I cant link to it sorry but I answered a similar question about and on June 3rd with: The square brackets denote a macro, this is really a part of the internals of lean not seen too often, so while I don't know a good reference, looking at tpil and the reference manual and mathlib docs suffices for normal notation.
To see what it really is we can ask lean to unfold the macro with a short metaprogram:

import tactic
open tactic
run_cmd (do
e ← get_env,
d ← get_decl `and.left,
trace $ e.unfold_all_macros d.value)

to see that the definition is really

λ (a b : Prop) (c : a ∧ b), and.rec (λ (left : a) (right : b), left) c

as for why it is written in this weird way, I can only assume there are some C-level efficiency reasons that this gets special treatment.