agda - 无法解析左侧 (m + 1) * n

Question

我刚开始学习 Agda 阅读 Programming Language Foundations in Agda .在第一章中有乘法的定义，其中一种情况是 (suc m) * n = n + (m * n)。我认为它可以更好地表达为 (m + 1) * n = n + (m * n)，但显然情况并非如此。以下程序:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

{-# BUILTIN NATURAL ℕ #-}

_*_ : ℕ → ℕ → ℕ
zero * n = zero
-- This is fine:
-- (suc m) * n = n + (m * n)
-- This is not:
(m + 1) * n = n + (m * n)

失败:

Could not parse the left-hand side (m + 1) * n
Operators used in the grammar:
  * (infix operator, level 20) [_*_ (/Users/proxi/Documents/Projekty/Agda/multiply.agda:11,1-4)]
  + (infix operator, level 20) [_+_ (/Users/proxi/Documents/Projekty/Agda/multiply.agda:5,1-4)] 
when scope checking the left-hand side (m + 1) * n in the
definition of _*_

我相信 Agda 的术语可以说使用构造函数的定义工作正常，但使用运算符的定义却不行。为什么呢？这是永远不可能的，还是取决于运算符(函数)的定义方式？

Answer 1

在模式中使用函数是 not supported .

另请注意，如果模式中允许使用函数，它将是 (1 + m) * n 而不是 (m + 1) * n，因为 _+_ 由第一个参数的模式匹配定义，因此 1 + m 简化为 suc m 和 m + 1 卡住了。