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/CHAD/Lemmas.hs | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 src/CHAD/Lemmas.hs

(limited to 'src/CHAD/Lemmas.hs')

diff --git a/src/CHAD/Lemmas.hs b/src/CHAD/Lemmas.hs
new file mode 100644
index 0000000..55ef042
--- /dev/null
+++ b/src/CHAD/Lemmas.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module CHAD.Lemmas (module CHAD.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