coq - Coq：本地 ltac 定义

Question

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

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

(* ll should not be visible here *)

Answer 1

您可以使用一个部分：

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