clickable notations - Githubissues

affeldt-aist / coq2html

An HTML documentation generator for Coq source files

GNU General Public License v2.0

1 stars 3 forks source link

clickable notations #4

Closed yoshihiro503 closed 8 months ago

yoshihiro503 commented 8 months ago

Changes:

list of notations in index
clickable notations
support for mobile phones
darkmode support
references of external library

Usage example

.
├── coq2html/
└── analysis/

../coq2html/coq2html -d html/ -base mathcomp -Q theories analysis -coqlib https://coq.inria.fr/doc/V8.18.0/stdlib/ -external https://math-comp.github.io/htmldoc/ mathcomp.ssreflect -external https://math-comp.github.io/htmldoc/ mathcomp.algebra classical/*.v classical/*.glob theories/*.v theories/*.glob

Demos

mathcomp analysis: https://yoshihiro503.github.io/coq2html/
monae: https://yoshihiro503.github.io/coq2html/monae-html/