tjh.dev
1{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
2
3mkCoqDerivation {
4
5 namePrefix = [ "coq" "mathcomp" ];
6 pname = "bigenough";
7 owner = "math-comp";
8
9 release = {
10 "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg";
11 "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
12 };
13 inherit version;
14 defaultVersion = with lib.versions; lib.switch coq.version [
15 { case = range "8.10" "8.17"; out = "1.0.1"; }
16 { case = range "8.5" "8.14"; out = "1.0.0"; }
17 ] null;
18
19 propagatedBuildInputs = [ mathcomp.ssreflect ];
20
21 meta = {
22 description = "A small library to do epsilon - N reasonning";
23 license = lib.licenses.cecill-b;
24 };
25}