{ description = "quox: quantitative extensional type theory";

  inputs = {
    nixpkgs.url = "nixpkgs";
    flake-utils.url = "github:numtide/flake-utils";

    idris2-pkgs = {
      url = "github:lizard-business/idris2-pkgs?ref=idris0.6.0"; # [fixme]
      # url = "github:claymager/idris2-pkgs";
      inputs.nixpkgs.follows = "nixpkgs";
      inputs.flake-utils.follows = "flake-utils";
    };

    tap = {
      url = "git+https://git.rhiannon.website/rhi/idris2-tap?ref=main";
      inputs.nixpkgs.follows = "nixpkgs";
      inputs.flake-utils.follows = "flake-utils";
      inputs.idris2-pkgs.follows = "idris2-pkgs";
    };
  };

  outputs = { self, nixpkgs, idris2-pkgs, flake-utils, tap }:
    let
      packagePaths = {
        quox-lib   = ./lib;
        quox       = ./exe;
        quox-tests = ./tests;
      };

      extraDeps = [ tap ];

      systems = with flake-utils.lib.system;
          [ x86_64-darwin x86_64-linux i686-linux ];
    in
    with builtins;
    flake-utils.lib.eachSystem systems (system:
      let
        basePkgs = import nixpkgs {
          inherit system;
          overlays = [ idris2-pkgs.overlay ];
        };
        builders = basePkgs.idris2-pkgs._builders;

        extraDepPkgs =
          foldl' (acc: pkg: acc // pkg.packages.${system}) { } extraDeps;
        mkPackage = name: path:
          builders.idrisPackage path { extraPkgs = extraDepPkgs // packages; };
        mkDevShell = _: pkg:
          basePkgs.mkShell { buildInputs = [ (builders.devEnv pkg) ]; };

        packages = mapAttrs mkPackage packagePaths;
        devShells = mapAttrs mkDevShell packages;
      in {
        inherit packages devShells;
        defaultPackage = packages.quox;
        devShell = devShells.quox-lib;
      }
    );
}