当我期望看到一个荒谬的模式时，我如何使用agda2 2模式来生成模式？
当我期望看到一个荒谬的模式时，我如何使用agda2 2模式来生成模式？
提问于 2017-11-06 17:54:47
例如，我们正在证明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 2模式的Emacs 25。
回答 1
Stack Overflow用户
回答已采纳
发布于 2017-11-07 12:22:35
好的，假设您从下面的配置开始：
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>，直到您到达一个荒谬的情况。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/47142928
复制相关文章
相似问题
腾讯云开发者
