nordic-dev.net/nixpkgs
nordic-dev.net/nixpkgs
2
0
Fork 0
mirror of https://github.com/NixOS/nixpkgs.git synced 2025-01-18 02:44:30 +00:00
Code Issues Packages Projects Releases Wiki Activity

coqPackages.aac-tactics: init

Browse Source
This commit is contained in:
Ben Siraphob 2021-05-09 22:49:12 +07:00 committed by Vincent Laporte
parent 354e005d6c
commit 915abd3f08
2 changed files with 47 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
pkgs/development/coq-modules/aac-tactics/default.nix Normal file
View File

@ -0,0 +1,46 @@
{ lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation {
pname = "aac-tactics";
releaseRev = v: "v${v}";
release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM=";
release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY=";
release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4=";
release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg=";
release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = "8.13"; out = "8.13.0"; }
{ case = "8.12"; out = "8.12.0"; }
{ case = "8.11"; out = "8.11.0"; }
{ case = "8.10"; out = "8.10.0"; }
{ case = "8.9"; out = "8.9.0"; }
{ case = "8.8"; out = "8.8.0"; }
{ case = "8.6"; out = "8.6.1"; }
{ case = "8.5"; out = "8.5.0"; }
] null;
mlPlugin = true;
meta = {
description = "Coq plugin providing tactics for rewriting universally quantified equations";
longDescription = ''
This Coq plugin provides tactics for rewriting universally quantified
equations, modulo associativity and commutativity of some operator.
The tactics can be applied for custom operators by registering the
operators and their properties as type class instances. Many common
operator instances, such as for Z binary arithmetic and booleans, are
provided with the plugin.
'';
maintainers = with maintainers; [ siraben ];
license = licenses.gpl3Plus;
platforms = platforms.unix;
};
}

1
pkgs/top-level/coq-packages.nix
View File

@ -13,6 +13,7 @@ let
contribs = recurseIntoAttrs
(callPackage ../development/coq-modules/contribs {});
aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
autosubst = callPackage ../development/coq-modules/autosubst {};
bignums = if lib.versionAtLeast coq.coq-version "8.6"
then callPackage ../development/coq-modules/bignums {}