nixpkgs/pkgs/top-level/agda-packages.nix

{ pkgs, lib, newScope, Agda }:

let
  mkAgdaPackages = Agda: lib.makeScope newScope (mkAgdaPackages' Agda);
  mkAgdaPackages' = Agda: self: let
    inherit (self) callPackage;
    inherit (callPackage ../build-support/agda {
      inherit Agda self;
      inherit (pkgs.haskellPackages) ghcWithPackages;
    }) withPackages mkLibraryFile mkDerivation;
  in {
    inherit mkLibraryFile mkDerivation;

    lib = lib.extend (final: prev: import ../build-support/agda/lib.nix { lib = prev; });

    agda = withPackages [];

    standard-library = callPackage ../development/libraries/agda/standard-library {
      inherit (pkgs.haskellPackages) ghcWithPackages;
    };

    iowa-stdlib = callPackage ../development/libraries/agda/iowa-stdlib { };

    agda-prelude = callPackage ../development/libraries/agda/agda-prelude { };

    agda-categories = callPackage ../development/libraries/agda/agda-categories { };

    cubical = callPackage ../development/libraries/agda/cubical { };

    functional-linear-algebra = callPackage
      ../development/libraries/agda/functional-linear-algebra { };

    generic = callPackage ../development/libraries/agda/generic { };

    agdarsec = callPackage ../development/libraries/agda/agdarsec { };

    _1lab = callPackage ../development/libraries/agda/1lab { };

    generics = callPackage ../development/libraries/agda/generics { };
  };
in mkAgdaPackages Agda