hydra-battles
hydra-battles copied to clipboard
coq-community
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Mentionned as https://github.com/cpitclaudel/alectryon/issues/94
Context: https://coq.zulipchat.com/#narrow/stream/344515-Hydras-.26-Co.2E-universe/topic/Good.20riddance.20to.20binders.20in.20index/near/319202524
I'm opening this as a memento to adapt Nix Toolbox CI to the new packaging of Gaia. Specifically, the Gaia Hydras package now only depends on the Gaia Schütte part...
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...
>@palmskog You were worried about CI length: it turns out that the CI job that was already the lengthiest (building the documentation) is impacted by the addition of Gaia as...
@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...
Metadata
Owner
Metadata
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]