what does this definition mean?

Stream: new members

[Ben Lee]

#print and.left

@[reducible]
def and.left : ∀ {a b : Prop}, a ∧ b → a :=
λ (a b : Prop) (c : a ∧ b), [and.left c]

Some questions:

1. I'm guessing this is not a circular definition, but how does it work?
2. What do the square braces around [and.left c] mean?
3. Meta-question: where do I learn about these syntax things? I searched through "Theorem proving with Lean" and the reference manual and couldn't find anything about square braces (besides lists.)

[Alex J. Best]

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.

[Alex J. Best]

Maybe docs#macro_def is the closest thing I know to documentation of this!

[Mario Carneiro]

It's a projection macro. Lean implements reduction for projections directly rather than using the recursor for efficiency.

[Mario Carneiro]

it is also ignored by #reduce (not expanded to the recursor), which is a kind of magic you can't achieve any other way

[Ben Lee]

Thanks for the pointers, that helps!