Attaching an attribute to a definition causes syntax errors

Question

I want to attribute a definition reducible. I am pretty sure I got the syntax right, as I copied it verbatim from the tutorial (p. 118).

definition pr1 [reducible] (A : Type) (a b : A) : A := a
attribute pr1 [reducible]

Neither combination of the two attributes pass the syntax check: Attaching it directly to the definition causes type expected at reducible, while the standalone declaration causes command expected.

I'm on Windows, using the Lean 3.1 binary distribution together with the VS Code language tooling, fwiw, but it doesn't seem to work in the browser either.

Answer 1

You are using an outdated version of the tutorial, the up-to-date one is here. You can use the following syntax:

@[reducible]
definition pr1 (A : Type) (a b : A) : A := a

or

attribute [reducible]
definition pr1 {A B : Type} (a : A) (b : B) := a

One can also assign the attribute any time after the definition takes place:

definition pr1 (A : Type) (a b : A) : A := a
-- some code
attribute [reducible] pr1