如何在Agda中使用with进行检查？

Question

我正在尝试从agda的编程基础上复制一个非常简单的coq证明，并告诉我我需要使用with with来证明模式匹配在字符串（布尔）可确定性上存在矛盾。我收到以下错误，并且文档甚至没有提供与with inspect一起使用的正确程序。为什么这种类型的推断不正确，如何解决我的错误？

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定义。