From 174af2ba568de66e0d890825b8bda930b8e7bb96 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Mon, 10 Nov 2025 21:49:45 +0100
Subject: Move module hierarchy under CHAD.

---
 src/Lemmas.hs | 21 ---------------------
 1 file changed, 21 deletions(-)
 delete mode 100644 src/Lemmas.hs

(limited to 'src/Lemmas.hs')

diff --git a/src/Lemmas.hs b/src/Lemmas.hs
deleted file mode 100644
index 31a43ed..0000000
--- a/src/Lemmas.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-{-# LANGUAGE AllowAmbiguousTypes #-}
-module Lemmas (module Lemmas, (:~:)(Refl)) where
-
-import Data.Type.Equality
-import Unsafe.Coerce (unsafeCoerce)
-
-
-type family Append a b where
-  Append '[] l = l
-  Append (x : xs) l = x : Append xs l
-
-lemAppendNil :: Append a '[] :~: a
-lemAppendNil = unsafeCoerce Refl
-
-lemAppendAssoc :: Append a (Append b c) :~: Append (Append a b) c
-lemAppendAssoc = unsafeCoerce Refl
-- 
cgit v1.2.3-70-g09d2