diff --git a/pkgs/development/libraries/agda/functional-linear-algebra/default.nix b/pkgs/development/libraries/agda/functional-linear-algebra/default.nix new file mode 100644 index 00000000000..dbcdaac532e --- /dev/null +++ b/pkgs/development/libraries/agda/functional-linear-algebra/default.nix @@ -0,0 +1,26 @@ +{ fetchFromGitHub, lib, stdenv, mkDerivation, standard-library }: + +mkDerivation rec { + version = "0.1"; + pname = "functional-linear-algebra"; + + buildInputs = [ standard-library ]; + + src = fetchFromGitHub { + repo = "functional-linear-algebra"; + owner = "ryanorendorff"; + rev = "v${version}"; + sha256 = "09ri3jmgp9jjwi1mzv4c3w6rvcmyx6spa2qxpwlcn0f4bmfva6wm"; + }; + + meta = with stdenv.lib; { + homepage = "https://github.com/ryanorendorff/functional-linear-algebra"; + description = '' + Formalizing linear algebra in Agda by representing matrices as functions + from one vector space to another. + ''; + license = licenses.bsd3; + platforms = platforms.unix; + maintainers = with maintainers; [ ryanorendorff ]; + }; +} diff --git a/pkgs/top-level/agda-packages.nix b/pkgs/top-level/agda-packages.nix index 3209aff9496..601ab6d42b9 100644 --- a/pkgs/top-level/agda-packages.nix +++ b/pkgs/top-level/agda-packages.nix @@ -25,6 +25,9 @@ let cubical = callPackage ../development/libraries/agda/cubical { }; + functional-linear-algebra = callPackage + ../development/libraries/agda/functional-linear-algebra { }; + generic = callPackage ../development/libraries/agda/generic { }; }; in mkAgdaPackages Agda