Что делает команда Coq Require Import Ltac?

Question

Когда я смотрю на проект QuickChick, я столкнулся с предложением Require Import Ltac. Я не знаю, что это делает и где Ltac Модуль есть. Я нашел файл plugins/ltac/Ltac.v, но это не могло быть так, поскольку этот файл пуст (кстати, зачем вообще включать пустой файл?). Я старался Locate Ltac. но я получил Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable])., что более запутанно.

Что это Ltac модуль до, где находится Ltac.v файл, и почему не Loacte Командная работа в этом случае? Спасибо!

Answer 1

Require Import Ltac. это действительно Coq.ltac.Ltac, пустой файл, который вы нашли! Я не уверен, почему там есть пустой файл, но он был представлен, когда Ltac был перемещен в плагин. Возможно, он служит в качестве заполнителя, если некоторые из реализаций Ltac были перемещены в Coq, а не как плагин OCaml. В любом случае я думаю, что у QuickChick нет особых причин импортировать его, если только они не ожидают каких-либо изменений в Coq, о которых я не знаю.

Из-за конфликта с народным командованием Locate Ltac (что дает вам синтаксическую ошибку), вам нужно вместо этого использовать Locate Module в явном виде. То же самое касается Print Module,

Locate Module Ltac отчеты Module Coq.ltac.Ltac, который говорит вам, что вы действительно смотрите на theories/ltac/Ltac.v, а также Print Module Ltac показывает пустой модуль. Однако этот второй бит вводит в заблуждение, поскольку то, что выглядит как пустые модули, все еще может иметь обозначения (здесь это не так, но только к сведению).