lean - 精益定义中的类型问题

Question

如果我做出定义

definition f (x : nat) := λ m, x + m

然后按预期#check f返回f:nat -> nat -> nat。

相反，如果我尝试定义

definition f (x : nat) : nat -> nat -> nat := λ m, x + m

然后 Lean 抱怨说 x 有 typenat但应该有 type nat -> nat。

为什么是这样？

Answer 1

基本上有三种定义方式f

def f (x m : nat) : nat := x + m

def f (x : nat) : nat -> nat := λ m, x + m

def f : nat -> nat -> nat := λ x m, x + m

这三个fs 的类型都是相同的，只是定义函数的语法不同。冒号左侧的所有内容都是函数的输入，冒号之后是返回类型。的术语 right:=应该有冒号后面的类型。在您的第二个示例中， the 之后的术语的类型:=是nat -> nat，但预期的类型是nat -> nat -> nat，因为这是冒号之后写的。所以出现了错误。

f如果您键入，则冒号左侧的所有参数都包含在类型中#check f。