Исключение доказательства при генерации HTML с использованием coqdoc - PullRequest
0 голосов
/ 22 марта 2020

Как видно из Книги по основам программного обеспечения , например, в главе Списки есть некоторые доказательства, которые исключены (поиск исключен на странице), и вы можете расширить их, нажав кнопка +. Я предполагаю, что эта книга написана с использованием coqdoc, поэтому при создании файла HTML должен быть способ исключить некоторые доказательства, которые я не могу найти. Я хочу создать документацию, в которой я предпочитаю исключить некоторые длинные доказательства и хотел бы знать, как это делается.

1 Ответ

1 голос
/ 22 марта 2020

Вы можете использовать coqdo cjs, чтобы сделать разборные доказательства в сгенерированном HTML.

Основы программного обеспечения делают это по-другому, с помощью собственных внутренних сценариев для настройки HTML, подставив некоторые специальные комментарии. Но конечный результат похож.

...