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]
While doing some proofreading of the pdf before, I noticed that the typeclasses in `ordinals` are seemingly using the so-called semibundled approach when defining typeclasses, and not the *unbundled* approach...
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),...
Metadata
Owner
Metadata
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]