coqPackages.hydra-battles: 0.3 -> 0.4

This commit is contained in:
Théo Zimmermann 2021-08-17 10:25:41 +02:00
parent 98e2339545
commit ff96901dbd
No known key found for this signature in database
GPG Key ID: F1744A0942F536C7

View File

@ -1,28 +1,32 @@
{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }:
{ lib, mkCoqDerivation, coq, equations, version ? null }:
with lib;
mkCoqDerivation {
pname = "hydra-battles";
owner = "coq-community";
release."0.3".rev = "v0.3";
release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg=";
release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
releaseRev = (v: "v${v}");
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.11"; out = "0.3"; }
{ case = isGe "8.11"; out = "0.4"; }
] null;
propagatedBuildInputs = [ mathcomp equations paramcoq ];
propagatedBuildInputs = [ equations ];
useDune2 = true;
meta = {
description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq";
description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
longDescription = ''
Variations on Kirby & Paris' hydra battles and other
entertaining math in Coq (collaborative, documented, includes
exercises)
An exploration of some properties of Kirby and Paris' hydra
battles, with the help of the Coq Proof assistant. This
development includes the study of several representations of
ordinal numbers, and a part of the so-called Ketonen and Solovay
machinery (combinatorial properties of epsilon0).
'';
maintainers = with maintainers; [ siraben ];
maintainers = with maintainers; [ siraben Zimmi48 ];
license = licenses.mit;
platforms = platforms.unix;
};