Pierre Castéran
Pierre Castéran
On branch utf8 I added a snippet `utf8try`at the end of `gaia/T1Bridge.v` with the utf8 character for omega. The file `movies/snippets/T1Bridge.tex` looks to be OK, but in `hydras.pdf` all the...
@start974 @Zimmi48 @palmskog @cpitclaudel The part of hydra-battles's documentation dedicated to ordinals is now made with Alectryon. (sniipets extracted from theories/ordinals/*/*.v ) This document is stiil a draft, and I...
In the files inherited from Goedel (now in theories/Ackermann), the predicates isPR and isPRrel are of sort Set, but all the proofs of primitive recursivity were opaque (endind by Qed),...
Looks like the link to mathcomp summer school leads to a winter school on classic Coq. https://team.inria.fr/marelle/en/coq-winter-school-2018/