问Coq:地方ltac定义
EN

Stack Overflow用户

提问于 2018-08-22 06:52:46

回答 1查看 170关注 0票数 2

如果有一种方法来定义一个“局部”Ltac表达式，我可以用它来证明一个引理，但在外面却看不见？

Lemma Foo ...
Proof.
   Ltac ll := ...
   destrict t.
   - reflexivity.
   - ll.
   - ll.
Qed.

(* ll should not be visible here *)

回答已采纳

发布于 2018-08-22 14:25:11

您可以使用以下部分：

Section Foo.
  Ltac solve := exact I.
  Lemma Foo : True.
  Proof.
    solve.
  Qed.
End Foo.

票数 5

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/51961226

复制

相似问题

问Coq:地方ltac定义EN