如何导入`∃-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

...将使其通过解析，但我不确定这是否正确解决了我要解决的问题之一。

我应该在这里做什么？

Answer 1

∃ 恰好适用于可以省略函数域的情况因为它很明显。否则你应该使用 Σ。确实 Σ-syntax 确实给了你写 Σ[ x ∈ A ] B.

的能力

如何导入`∃-syntax`？

How to import the `∃-syntax`?

agda