Как я могу использовать agda2-mode для генерации паттернов, когда ожидаю увидеть абсурдный паттерн?

Question

Например, мы доказываем 2 + 2 != 5:

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  znn : ∀ {n} → zero + n ≡ n
  sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k

И я могу доказать это вручную:

2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 (sns (sns ()))

Но я хочу шаблон (sns (sns ())) быть сгенерированным (так же, как заполнение дыры). Есть ли способы добиться этого?

Я использую Emacs 25 с agda2-режимом.

Answer 1

Итак, допустим, вы начинаете с этой конфигурации:

2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 h = {!!}

В этом случае вы можете использовать макросы клавиатуры emacs, потому что подстрок генерируется путем сопоставления с h также будет назван h, Итак, используя:

• <f3> (начать запись макроса)
• C-c C-f (перейти к отверстию)
• C-c C-c h RET (матч на h)
• <f4> (запишите макрос)

Вы записали действие "переход к первой цели, совпадающей на h". Теперь вы можете продолжать нажимать <f4> пока вы не дойдете до абсурда.