Agda：无法解析应用程序

Question

当我尝试从 Agda 中的编程语言基础加载此示例时，它失败了：

module Test where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _∎; _≡⟨⟩_)

data Nat : Set where
    zero : Nat
    suc : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

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

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

第一次警告：

warning: -W[no]ModuleDoesntExport
The module Eq.≡-Reasoning doesn't export the following:
  _≡⟨⟩_
when scope checking the declaration
  open Eq.≡-Reasoning using (begin_; _∎; _≡⟨⟩_)

第二个错误：

Could not parse the application
begin 2 + 3 ≡ (suc (suc zero)) + (suc (suc (suc zero))) ≡ suc
((suc zero) + (suc (suc (suc zero)))) ≡ suc
(suc (zero + (suc (suc (suc zero))))) ≡ suc
(suc (suc (suc (suc zero)))) ≡ 5 ∎
Operators used in the grammar:
  +     (infix operator, level 20)  [_+_ (C:\Users\user\Documents\Agda\VSC\Test.agda:12,1-4)]                                                                            
  ∎     (postfix operator, level 3) [_∎ (C:\cabal\agda-stdlib-2.0\src\Relation\Binary\Reasoning\Syntax.agda:442,3-5)]                                                     
  ≡     (infix operator, level 4)   [_≡_ (C:\cabal\store\ghc-9.4.8\Agda-2.6.4.1-e51cf1324caf3a56d7db642f01cda06d05fc0698\share\lib\prim\Agda\Builtin\Equality.agda:6,6-9)]
  begin (prefix operator, level 1)  [begin_ (C:\cabal\agda-stdlib-2.0\src\Relation\Binary\Reasoning\Syntax.agda:51,3-9)]                                                  
when scope checking
begin 2 + 3 ≡ (suc (suc zero)) + (suc (suc (suc zero))) ≡ suc
((suc zero) + (suc (suc (suc zero)))) ≡ suc
(suc (zero + (suc (suc (suc zero))))) ≡ suc
(suc (suc (suc (suc zero)))) ≡ 5 ∎

我正在使用Agda标准库2.0，我注意到运算符≡⟨⟩不再位于Relation.Binary.PropositionalEquality中（与1.7.2相比），但我找不到任何替换。另外我不确定运算符“QI⟨⟩”是什么意思，或者hoagw可以替换它，但我也不确定这是否真的是它无法加载的原因。

Answer 1

这是标准库 v2.0 的问题:

我刚刚研究过这个。根本问题不是 ≡⟨⟩ 有 已被删除，但它现在被声明为不同的语法 name，这会破坏仅使用某些名称打开 Equi-Reasoning 模块 按照 PLFA 的指示。我同意这很不幸。

同时，您可以使用 (begin_; 替换开放式方程-推理) ≡⟨⟩； ❖) 并使用 (begin;step-❖-∣;_❖) 进行开放式 ≡ 推理。 stdlib 中的约定是不对各种变量使用 using 子句 推理模块，这就是为什么我们直到现在才注意到。

解决方案是使用标准库 1.7.3 或等待修复。