mirror of
https://github.com/NixOS/nixpkgs.git
synced 2025-01-28 07:43:43 +00:00
755b915a15
nix run nixpkgs#silver-searcher -- -G '\.nix$' -0l 'description.*"[Aa]n?' pkgs \ | xargs -0 nix run nixpkgs#gnused -- -i '' -Ee 's/(description.*")[Aa]n? (.)/\1\U\2/'
24 lines
769 B
Nix
24 lines
769 B
Nix
{ coq, mkCoqDerivation, mathcomp, coqeal, mathcomp-real-closed,
|
|
mathcomp-bigenough, mathcomp-zify, mathcomp-algebra-tactics,
|
|
lib, version ? null }:
|
|
|
|
mkCoqDerivation {
|
|
|
|
pname = "apery";
|
|
|
|
inherit version;
|
|
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
|
{ cases = [ (range "8.13" "8.16") (range "1.12.0" "1.17.0") ]; out = "1.0.2"; }
|
|
] null;
|
|
|
|
release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
|
|
|
|
propagatedBuildInputs = [ mathcomp.field coqeal mathcomp-real-closed
|
|
mathcomp-bigenough mathcomp-zify mathcomp-algebra-tactics ];
|
|
|
|
meta = {
|
|
description = "Formally verified proof in Coq, by computer algebra, that ζ(3) is irrational";
|
|
license = lib.licenses.cecill-c;
|
|
};
|
|
}
|