Как да получите синтактични декларации, които да се използват чрез разделяне на главни и малки букви

Бих искал автоматично да добавя регистър към аргументите, използвайки синтаксис, деклариран освен дадения като конструктор на тип. Например,

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

не успее, където ─ се произвежда от \---

)