Jason Gross
Jason Gross
We now have documentation with [Alectryon](https://plv.csail.mit.edu/blog/alectryon.html). (TOC [here](https://hott.github.io/HoTT/alectryon-html/toc.html), index [here](https://hott.github.io/HoTT/alectryon-html/), and note that the rest of the pages are much, much prettier than the jank index and TOC) The blog...
It would be nice to be able to browse the build artifacts (especially the proviola one) on a PR. I'm not sure how to do this; the setup that Coq...
We should consider consolidating `erapply` and `rapply` into a single tactic without an argument length limit, as @jonleivent recently suggested on coqdev: ``` coq Tactic Notation "is_valid_open_constr" uconstr(term) := try...
In particular, it would be nice to have [this toc](http://hott.github.io/HoTT/timing-html/toc.html) annotated with timing info. The relevant target of [the Makefile](https://github.com/HoTT/HoTT/blob/master/Makefile.am) is `timing-html/toc.html`.
The tactic `transport_path_forall_hammer` in `Tactics.v` should probably be better documented, similar to the first `issig` tactic in `types/Record.v`. I might go try to do this at some point, but I...
Should we make more notations for equivalences, like `+` for `equiv_functor_sum'` and `*` for `equiv_functor_prod'` and `->` for `equiv_functor_arrow'`, etc?
We should add the following to Overture: ``` coq (** This command makes [simpl] more well-behaved. For example, it makes [simpl] better at re-folding fixpoints and respecting [Arguments] commands. *)...
I'm designing a week-long class on homotopy type theory for Mathcamp, and in trying to simplify the material, noticed that the essential insight to the proofs of the following two...
The following works fine: ```latex \documentclass{article} \usepackage{minted} \begin{document} $\mintinline{c}{void foo}$ \end{document} ``` If instead I run ```latex \documentclass{article} \usepackage{minted} \setmintedinline{breaklines} \begin{document} $\mintinline{c}{void foo}$ \end{document} ``` I get ``` $ pdflatex...
I have ```tex \documentclass{article} \usepackage{hyperref} \begin{document} \begin{Form} \fbox{\CheckBox[name=foo,checked=true]{}} \end{Form} \end{document} ``` This checkbox shows up fine in Adobe Reader, but the checkbox is unchecked in Chrome's PDF viewer, and does...