How to get syntax declarations to be used by case splitting

Question

I would like to automatically case over arguments using a syntax declared besides the one given as a type constructor. For example,

postulate P : ℕ → ℕ → Set

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

Here, I'd like to have the proof P n m occur between the n and m arguments, but that cannot be since both need to be declare for it to be expressed. Hence, we use a syntax declaration:

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

Now, we can write-up by-hand

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

This works fine, but when I case-split via C-c C-c, it uses goo instead of my syntax. Is there any way to make case splitting use my declared syntax ?

( Incidentally, using

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

fails, where ─ is produced by \---

)

Jagannath

The version using \--- works with Agda 2.4.2.5. – Volitive

Answer 1

Nowadays Agda resugars patterns on the left if they are in scope unqualified so this would just work.

Pensive

An example or link demonstrating an example would be helpful for people who land at this page ;-) – Jagannath