定義に属性を添付すると、構文エラーが発生する

Question

定義を属性にしたいreducible。 tutorial (p. 118)から逐語的にコピーしたので、私は構文が正しいと確信しています。

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

二つの属性のいずれもの組み合わせは、構文チェックに合格：定義に直接取り付けスタンドアローン宣言がcommand expectedを引き起こしながら、type expected at reducibleを引き起こします。

私はWindows上で、Lean 3.1バイナリディストリビューションとVSコード言語ツールfwiwを併用していますが、ブラウザでも動作しないようです。

Answer 1

このチュートリアルの古いバージョンを使用していますが、最新のものはhereです。あなたは、次の構文を使用することができます。

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

または

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

は

一つの定義が行われた後も、属性をいつでも割り当てることができます。

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