Agda定义幂运算符时出现解析错误，请求技术帮助

你的代码存在几处语法和格式问题，导致了解析错误，修复后的完整代码如下，我会逐一说明问题点：

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
data N : Set where
  zero : N
  suc : N → N
{-# BUILTIN NATURAL N #-}

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

_*_ : N → N → N
zero * n = zero
(suc m) * n = n + (m * n)

one = suc zero
_^_ : N → N → N
m ^ zero = one
m ^ (suc n) = m * (m ^ n)

错误原因说明 #

• 缩进不规范：Agda对缩进要求严格，所有函数子句的缩进必须统一，原代码中_+_、_*_、_^_的子句缩进不一致，直接触发解析失败。
• 变量名误用：_*_定义里的zero * N = zero，N是你定义的自然数类型，不是变量，需改为zero * n = zero。
• 模式匹配错误：m ^ (1 + n)不符合Agda的模式匹配规则，自然数的递归模式应基于构造子suc，而非用已定义的one做加法，改用m ^ (suc n)才是正确的递归写法。

修复后代码可正常通过解析，你可以运行测试验证。

内容的提问来源于stack exchange，提问作者Mirage