在 Agda 中,需要在函数名和参数之间使用“空格”来表示应用关系。因此,并不需要在每个参数之间放置额外的符号。
例如,对于以下函数定义:
f : Nat -> Nat -> Nat
f x y = x + y
应该使用以下语法来调用该函数:
f 1 2
而不是以下语法:
f(1, 2)
在 Agda 中,使用逗号分隔参数会被视为元组类型。因此,“f(1, 2)”表示一个类型为“(Nat,Nat)-> Nat”的函数类型,而不是我们想要的“Nat -> Nat -> Nat”函数类型。
下一篇:Agda的类型检查器爆炸了