pyrox.dev
lol
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 equations,
6 LibHyps,
7 version ? null,
8}:
9
10(mkCoqDerivation {
11 pname = "hydra-battles";
12 owner = "coq-community";
13
14 release."0.4".sha256 = "1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
15 release."0.5".sha256 = "121pcbn6v59l0c165ha9n00whbddpy11npx2y9cn7g879sfk2nqk";
16 release."0.6".sha256 = "1dri4sisa7mhclf8w4kw7ixs5zxm8xyjr034r1377p96rdk3jj0j";
17 release."0.9".sha256 = "sha256-wlK+154owQD/03FB669KCjyQlL2YOXLCi0KLSo0DOwc=";
18 releaseRev = (v: "v${v}");
19
20 inherit version;
21 defaultVersion =
22 with lib.versions;
23 lib.switch coq.coq-version [
24 {
25 case = range "8.13" "8.16";
26 out = "0.9";
27 }
28 {
29 case = range "8.11" "8.12";
30 out = "0.4";
31 }
32 ] null;
33
34 useDune = true;
35
36 meta = with lib; {
37 description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
38 longDescription = ''
39 An exploration of some properties of Kirby and Paris' hydra
40 battles, with the help of the Coq Proof assistant. This
41 development includes the study of several representations of
42 ordinal numbers, and a part of the so-called Ketonen and Solovay
43 machinery (combinatorial properties of epsilon0).
44 '';
45 maintainers = with maintainers; [
46 siraben
47 Zimmi48
48 ];
49 license = licenses.mit;
50 platforms = platforms.unix;
51 };
52}).overrideAttrs
53 (
54 o:
55 let
56 inherit (o) version;
57 in
58 {
59 propagatedBuildInputs = [
60 equations
61 ] ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
62 }
63 )