From 7df8575a723abaac022fa6bbd77aba66b96631f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kier=C3=A1n=20Meinhardt?= <kieran.meinhardt@gmail.com>
Date: Tue, 24 Sep 2019 17:01:21 +0200
Subject: [PATCH 1/2] idrisPackages.heyting-algebra: mark as broken

The functionality provided by this package has been added to the Idris contrib library (module `Interfaces.Verified`).
Therefore identifiers cannot be disambiguated anymore.
---
 pkgs/development/idris-modules/heyting-algebra.nix | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/pkgs/development/idris-modules/heyting-algebra.nix b/pkgs/development/idris-modules/heyting-algebra.nix
index 3fa546466c8a..e6656545cbe9 100644
--- a/pkgs/development/idris-modules/heyting-algebra.nix
+++ b/pkgs/development/idris-modules/heyting-algebra.nix
@@ -22,4 +22,6 @@ build-idris-package  {
     license = lib.licenses.mit;
     maintainers = [ lib.maintainers.brainrape ];
   };
+
+  broken = true;
 }

From 8eb0413c05df225fa697d3d413bfa25158d753ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kier=C3=A1n=20Meinhardt?= <kieran.meinhardt@gmail.com>
Date: Tue, 24 Sep 2019 19:49:25 +0200
Subject: [PATCH 2/2] idrisPackages.heyting-algebra: remove

---
 pkgs/development/idris-modules/default.nix    |  2 --
 .../idris-modules/heyting-algebra.nix         | 27 -------------------
 2 files changed, 29 deletions(-)
 delete mode 100644 pkgs/development/idris-modules/heyting-algebra.nix

diff --git a/pkgs/development/idris-modules/default.nix b/pkgs/development/idris-modules/default.nix
index 47c6998a587d..074a260b8169 100644
--- a/pkgs/development/idris-modules/default.nix
+++ b/pkgs/development/idris-modules/default.nix
@@ -103,8 +103,6 @@
 
     html = callPackage ./html.nix {};
 
-    heyting-algebra = callPackage ./heyting-algebra.nix {};
-
     hezarfen = callPackage ./hezarfen.nix {};
 
     hrtime = callPackage ./hrtime.nix {};
diff --git a/pkgs/development/idris-modules/heyting-algebra.nix b/pkgs/development/idris-modules/heyting-algebra.nix
deleted file mode 100644
index e6656545cbe9..000000000000
--- a/pkgs/development/idris-modules/heyting-algebra.nix
+++ /dev/null
@@ -1,27 +0,0 @@
-{ build-idris-package
-, fetchFromGitHub
-, contrib
-, lib
-}:
-build-idris-package  {
-  name = "heyting-algebra";
-  version = "2017-08-18";
-
-  idrisDeps = [ contrib ];
-
-  src = fetchFromGitHub {
-    owner = "Risto-Stevcev";
-    repo = "idris-heyting-algebra";
-    rev = "2c814c48246a5e19bff66e64a753208c7d59d397";
-    sha256 = "199cvhxiimlhchvsc66zwn0dls78f9lamam256ad65mv4cjmxv40";
-  };
-
-  meta = {
-    description = "Interfaces for heyting algebras and verified bounded join and meet semilattices";
-    homepage = https://github.com/Risto-Stevcev/idris-heyting-algebra;
-    license = lib.licenses.mit;
-    maintainers = [ lib.maintainers.brainrape ];
-  };
-
-  broken = true;
-}