diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix new file mode 100644 index 00000000000..a74eec4b64f --- /dev/null +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -0,0 +1,29 @@ +{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, 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="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "0.3"; } + ] null; + + propagatedBuildInputs = [ mathcomp equations paramcoq ]; + + meta = { + description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq"; + longDescription = '' + Variations on Kirby & Paris' hydra battles and other + entertaining math in Coq (collaborative, documented, includes + exercises) + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 6da0598c6ac..2a6c9d42377 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -39,6 +39,7 @@ let heq = callPackage ../development/coq-modules/heq {}; hierarchy-builder = callPackage ../development/coq-modules/hierarchy-builder {}; HoTT = callPackage ../development/coq-modules/HoTT {}; + hydra-battles = callPackage ../development/coq-modules/hydra-battles {}; interval = callPackage ../development/coq-modules/interval {}; InfSeqExt = callPackage ../development/coq-modules/InfSeqExt {}; iris = callPackage ../development/coq-modules/iris {};