Coq: локальное определение ltac

Если есть способ определить "локальное" выражение Ltac, которое я могу использовать для доказательства леммы, но не видимый снаружи?

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

(* ll should not be visible here *)
Источник

1 ответ

Решение

Вы можете использовать раздел:

Section Foo.
  Ltac solve := exact I.
  Lemma Foo : True.
  Proof.
    solve.
  Qed.
End Foo.
Источник
Другие вопросы по тегам