pkgs/development/coq-modules/hydra-battles/default.nix

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