如何导入`∃-syntax`？

Question

open import Data.Product using (_×_; ∃; ∃-syntax)
open import Data.List

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → ∃[ x ∈ xs ] P x

Could not parse the application ∃[ x ∈ xs ] P x
Operators used in the grammar:
  ∃[_] (prefix notation, level 20) [∃-syntax (C:\Users\Marko\AppData\Roaming\cabal\x86_64-windows-ghc-8.6.5\Agda-2.6.0\lib\agda-stdlib\src\Data\Product.agda:78,1-9)]
when scope checking ∃[ x ∈ xs ] P x

由于某些原因，它似乎没有正确地从标准库模块导入优先级。定义为..。

Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → ∃[ x ] P x

...will让它通过解析，但是我不确定这对于我试图解决的一个问题是不是正确的。

我应该在这里做什么？

Answer 1

∃恰恰适用于可以省略函数域的情况，因为这是显而易见的。否则，您应该使用Σ。实际上，Σ-syntax确实提供了编写Σ[ x ∈ A ] B的能力。