当我期望看到荒谬的模式时，如何使用 agda2-mode 生成模式？
How can I use agda2-mode to generate patterns when I expect to see an absurd pattern?
例如，我们要证明 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 ()))（就像填洞一样）。有什么方法可以实现吗？
我正在使用带有 agda2-mode 的 Emacs 25。
好的，假设您从这个配置开始：
2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 h = {!!}
在这种情况下，您可以使用 emacs 的 keyboard macros，因为在 h 上匹配生成的子项也将被命名为 h。所以使用：
<f3>（开始录制宏）C-c C-f（移动到洞口）C-c C-c h RET（匹配 h）<f4>（录制宏）
您已经记录了 "moving to the first goal an matching on h" 的动作。您现在可以一直按 <f4> 直到出现荒谬的情况。
例如，我们要证明 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 ()))（就像填洞一样）。有什么方法可以实现吗？
我正在使用带有 agda2-mode 的 Emacs 25。
好的，假设您从这个配置开始：
2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 h = {!!}
在这种情况下，您可以使用 emacs 的 keyboard macros，因为在 h 上匹配生成的子项也将被命名为 h。所以使用：
<f3>（开始录制宏）C-c C-f（移动到洞口）C-c C-c h RET（匹配h）<f4>（录制宏）
您已经记录了 "moving to the first goal an matching on h" 的动作。您现在可以一直按 <f4> 直到出现荒谬的情况。