Commit 695b7ae9 authored by Pierre Roux's avatar Pierre Roux Committed by Vincent Laporte
Browse files

coqPackages.itree-io: init at 0.1.1

parent edcb325f
Loading
Loading
Loading
Loading
+24 −0
Original line number Diff line number Diff line
{ lib, mkCoqDerivation, coq, ITree, simple-io, version ? null }:

mkCoqDerivation {
  pname = "itree-io";
  repo = "coq-itree-io";
  owner = "Lysxia";
  inherit version;

  defaultVersion = let inherit (lib.versions) range; in
    lib.switch coq.coq-version [
      { case = range "8.12" "8.19"; out = "0.1.1"; }
    ] null;
  release = {
    "0.1.1".sha256  = "sha256-IFwIj8dxW4jm2gvuUJ8LKZFSJeljp0bsn8fezxY6t2o=";
  };
  releaseRev = v: "v${v}";

  propagatedBuildInputs = [ ITree simple-io ];

  meta = {
    description = "Interpret itree in the IO monad of simple-io.";
    license = lib.licenses.mit;
  };
}
+1 −0
Original line number Diff line number Diff line
@@ -79,6 +79,7 @@ let
      iris-named-props = callPackage ../development/coq-modules/iris-named-props {};
      itauto = callPackage ../development/coq-modules/itauto { };
      ITree = callPackage ../development/coq-modules/ITree { };
      itree-io = callPackage ../development/coq-modules/itree-io { };
      LibHyps = callPackage ../development/coq-modules/LibHyps {};
      ltac2 = callPackage ../development/coq-modules/ltac2 {};
      math-classes = callPackage ../development/coq-modules/math-classes { };