From 04ce88ce93523988ec1dc6775ac6a4b439e90913 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Wed, 24 Jan 2024 21:31:24 +0100
Subject: WIP rewrite code transform typing

---
 src/Lemmas.hs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 src/Lemmas.hs

(limited to 'src/Lemmas.hs')

diff --git a/src/Lemmas.hs b/src/Lemmas.hs
new file mode 100644
index 0000000..7dbf680
--- /dev/null
+++ b/src/Lemmas.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE PolyKinds #-}
+
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Lemmas (module Lemmas, (:~:)(Refl)) where
+
+import Data.Type.Equality
+import Unsafe.Coerce (unsafeCoerce)
+
+import AST.Weaken
+
+
+lemAppendAssoc :: Append a (Append b c) :~: Append (Append a b) c
+lemAppendAssoc = unsafeCoerce Refl
-- 
cgit v1.2.3-70-g09d2