coqPackages.odd-order: init at 1.12.0
This commit is contained in:
parent
d4ad51086d
commit
80d5498aa2
24
pkgs/development/coq-modules/odd-order/default.nix
Normal file
24
pkgs/development/coq-modules/odd-order/default.nix
Normal file
@ -0,0 +1,24 @@
|
||||
{ lib, mkCoqDerivation, mathcomp, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "odd-order";
|
||||
owner = "math-comp";
|
||||
|
||||
release."1.12.0".rev = "mathcomp-odd-order.1.12.0";
|
||||
release."1.12.0".sha256 = "sha256-omsfdc294CxKAHNMMeqJCcVimvyRCHgxcQ4NJOWSfNM=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch mathcomp.character.version [
|
||||
{ case = pred.union (isGe "1.10.0") (isEq "dev"); out = "1.12.0"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp.character ];
|
||||
|
||||
meta = {
|
||||
description = "Formal proof of the Odd Order Theorem";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.cecill-b;
|
||||
platforms = platforms.unix;
|
||||
};
|
||||
}
|
@ -58,6 +58,7 @@ let
|
||||
mathcomp-real-closed = callPackage ../development/coq-modules/mathcomp-real-closed {};
|
||||
metalib = callPackage ../development/coq-modules/metalib { };
|
||||
multinomials = callPackage ../development/coq-modules/multinomials {};
|
||||
odd-order = callPackage ../development/coq-modules/odd-order { };
|
||||
paco = callPackage ../development/coq-modules/paco {};
|
||||
paramcoq = callPackage ../development/coq-modules/paramcoq {};
|
||||
QuickChick = callPackage ../development/coq-modules/QuickChick {};
|
||||
|
Loading…
Reference in New Issue
Block a user