coqltac

Coq: local ltac definition


If there is a way to define a "local" Ltac expresion which I can use to proof a lemma but not visible outside?

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

(* ll should not be visible here *)

Solution

  • You can use a section:

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