不条理なパターンが見込まれると、パターンを生成するために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()))が発生することにしたいです。それを達成する方法はありますか？

私はagda2モードでEmacs 25を使用しています。

Answer 1

オクラホマので、あなたはこの構成から始めましょう：

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

この場合hに照合することによって生成されたサブ用語はまた、hという名前になりますので、あなたがEmacsのkeyboard macrosを使用することができます。そう使用：

• <f3>（マクロの記録を開始）
• C-c C-f（ホールに移動）
• C-c C-c h RET（hに一致）
• <f4>（マクロを記録する）

あなたは "最初のゴールへのマッチング"のアクションを記録しました。あなたは不条理なケースに達するまで<f4>を押し続けることができます。