emacs - 如何获取要由大小写拆分使用的语法声明

Question

我想使用声明的语法自动区分参数
除了作为类型构造函数给出的那个。例如，

postulate P : ℕ → ℕ → Set

data Silly : Set where
  goo : (n : ℕ) → Fin n → (m : ℕ) → Fin m → P n m → Silly

在这里，我想要证明 P n m发生在 n 之间和 m参数，但这不能，因为两者都需要声明才能表达。因此，我们使用语法声明:

syntax goo n i m j pf = i ⟵[ n , pf , m ]⟶ j

现在，我们可以手写

want-to-use-syntax-in-pattern-matching : Silly → Set
want-to-use-syntax-in-pattern-matching (i ⟵[ n , pf , m ]⟶ j) = ℕ

这工作正常，但是当我通过 C-c C-c 进行案例拆分时，它使用 goo而不是我的语法。有什么方法可以使用我声明的语法进行大小写拆分吗？

(
顺便说一句，使用

syntax goo n i m j pf = i ─[ n , pf , m ]⟶ j

失败，其中 ─由 \--- 制作

)

Answer 1

现在 Agda 会在左侧显示不合格的模式
所以这会起作用。