Agda加载《Programming Language Foundations in Agda》示例失败求助

开发者阿泽

2026-6-29

解决Agda标准库2.0适配《Programming Language Foundations in Agda》代码的问题

核心原因

Agda标准库2.0确实移除了Eq.≡-Reasoning模块中的_≡⟨⟩_运算符，这个原本用于等式推理链占位的空步骤符号被移除后，直接调用就会触发你看到的解析错误，这就是问题的根源。

直接省略空步骤：如果代码里_≡⟨⟩_只是用来占位、没有实际证明内容，直接删掉即可。比如原代码：
```
x ≡⟨⟩
y ≡⟨ refl ⟩
z ∎
```
修改后：
```
x ≡⟨ refl ⟩
y ∎
```
用_≡⟨ refl ⟩_替代：要是想保留步骤结构的可读性，用_≡⟨ refl ⟩_替换空的_≡⟨⟩_就行——refl是自反性证明，和空步骤语义完全一致：
```
x ≡⟨ refl ⟩
y ≡⟨ some-proof ⟩
z ∎
```
自定义空步骤运算符：如果习惯旧写法，可以自己在代码模块里定义一个和旧版_≡⟨⟩_功能相同的运算符：
```
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≡⟨_⟩_; _∎)

_≡⟨⟩_ : ∀ {a} {A : Set a} (x y : A) → x ≡ y → x ≡ y
x ≡⟨⟩ y p = p
```
定义后就能像以前一样使用_≡⟨⟩_了。