leanprover / reference-manual

Apache License 2.0
26 stars 3 forks source link

Attributes #144

Open david-christiansen opened 2 weeks ago

david-christiansen commented 2 weeks ago

What question should the reference manual answer?

What is the concrete syntax of attributes? What is the purpose of attributes in Lean? How is their scoping managed? When can they be added?