From 3a23bd851fc1a5d6e161dabc8a13f06bc8544a1d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 9 Sep 2024 11:33:45 +0100 Subject: Restart. - use De Bruijn, as Namely, Painless had more pain than promised; - remove higher-kinded types; - provide ill-typing predicates; - prove substitution respects ill-typing; --- src/Inky/Erased.idr | 6 ------ 1 file changed, 6 deletions(-) delete mode 100644 src/Inky/Erased.idr (limited to 'src/Inky/Erased.idr') diff --git a/src/Inky/Erased.idr b/src/Inky/Erased.idr deleted file mode 100644 index 05bb29e..0000000 --- a/src/Inky/Erased.idr +++ /dev/null @@ -1,6 +0,0 @@ -module Inky.Erased - -public export -record Erased (t : Type) where - constructor Forget - 0 val : t -- cgit v1.2.3