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   releaseRev = (v: "v${v}");
  11
  12   inherit version;
  13   defaultVersion = with lib.versions; lib.switch coq.coq-version [
  14     { case = range "8.13" "8.16"; out = "0.6"; }
  15     { case = range "8.11" "8.12"; out = "0.4"; }
  16   ] null;
  17
  18   useDune = true;
  19
  20   meta = with lib; {
  21     description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
  22     longDescription = ''
  23       An exploration of some properties of Kirby and Paris' hydra
  24       battles, with the help of the Coq Proof assistant. This
  25       development includes the study of several representations of
  26       ordinal numbers, and a part of the so-called Ketonen and Solovay
  27       machinery (combinatorial properties of epsilon0).
  28     '';
  29     maintainers = with maintainers; [ siraben Zimmi48 ];
  30     license = licenses.mit;
  31     platforms = platforms.unix;
  32   };
  33 }).overrideAttrs(o:
  34   let inherit (o) version; in {
  35     propagatedBuildInputs = [ equations ] ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
  36   })