Yeah it's really more of a full build system, quite overkill for just blogging.
I wrote poetry... in #Haskell...
I'm pretty sure all it takes is just starting something, but as always people are busy.
Although I have no idea what documentation in Coq should look like to account for dependent types.
I would also really like to work on that!
I really want to get involve in a community effort to give #Coq better documentation tooling.
TIL sha512 is faster than sha256 on 64bit machines and you can see it for yourself with a single command:
openssl speed sha256 sha512
Free applicative functors in #Coq, in a bleak world without functional extensionality
I am doing it anyway… and it’s funny to rework on my article about generalized rewriting two years later.
If I’ve learned one thing, is that the less vernacular command, the better. So:
1/ Use #[program] instead of Program
2/ Use #[program] Instance _: Equivalence _ instead of Add Parametric Relation
3/ Use #[program] Instance _: Proper (_ ==> _) _ instead of Add Parametric Morphism
I always need to copy/paste when using Add Parametric Relation/Morphism, never with Instance.