syntax - 将属性附加到定义会导致语法错误

Question

我想赋予一个定义reducible。我很确定我的语法是正确的，因为我从教程 (p. 118)中逐字复制了它。

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

这两个属性的组合都没有通过语法检查：将其直接附加到定义会导致type expected at reducible，而独立声明会导致command expected。

我在 Windows 上，使用 Lean 3.1 二进制发行版和 VS Code 语言工具 fwiw，但它似乎在浏览器中也不起作用。

score 1 · Accepted Answer

您正在使用本教程的过时版本，最新版本在这里。您可以使用以下语法：

@[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

1 回答 1