pattern-matching - 在 Agda 中如何使用 with 检查？

Question

我正在尝试从 agda 的编程基础中重现一个非常简单的 coq 证明，并被告知我需要使用 with 检查来证明与字符串本身的( bool )可判定性上的模式匹配的矛盾。我收到以下错误，文档甚至没有提供与检查一起使用的正确程序。为什么这种类型推断不正确，我该如何解决我的错误？

module Maps where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; subst; trans; sym; inspect)
open import Data.String using (_++_; _==_; _≟_; String)
open import Data.Bool using (T; Bool; true; false; if_then_else_)

-- Coq-- Theorem eqb_string_refl : forall s : string, true = eqb_string s s.
eqbstringrefl' : (s : String) →  true ≡ (s == s)
eqbstringrefl' s with inspect (s == s) 
... | false with≡ eq = {!!}
... | true with≡ eq  = {!!}

(s == s) 以红色突出显示并产生以下错误

Bool !=< (x : _A_70) → _B_71 x of type Set
when checking that the inferred type of an application
Bool
matches the expected type
(x : _A_70) → _B_71 x

Answer 1

inspect标准库中的函数具有以下类型:

inspect : ∀ {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x

如您所见，它需要两个显式参数:一个函数 f和一个值 x . user manual有一节介绍了如何使用检查习语，特别是第二个示例使用了与 inspect 基本相同的定义作为标准库。