如何获取案例拆分使用的语法声明

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) = ?

这工作正常,但是当我通过case分割时C-c C-c,它使用goo而不是我的语法.有没有办法让case拆分使用我声明的语法？

(顺便说一句,使用

syntax goo n i m j pf = i ?[ n , pf , m ]? j

失败,?产生于何处\---

)

Answer 1

如今，如果左侧的模式在不合格的范围内，Agda 会重新调整左侧的模式，因此这将起作用。