From 7d44dcc2ca2c5c16e1ab4737ef6b2877214767ed Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Mon, 2 Sep 2024 17:49:54 +0200
Subject: WIP autoWeak

---
 src/Lemmas.hs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'src/Lemmas.hs')

diff --git a/src/Lemmas.hs b/src/Lemmas.hs
index cb62155..31a43ed 100644
--- a/src/Lemmas.hs
+++ b/src/Lemmas.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 {-# LANGUAGE AllowAmbiguousTypes #-}
 module Lemmas (module Lemmas, (:~:)(Refl)) where
@@ -8,8 +9,10 @@ module Lemmas (module Lemmas, (:~:)(Refl)) where
 import Data.Type.Equality
 import Unsafe.Coerce (unsafeCoerce)
 
-import AST.Weaken
 
+type family Append a b where
+  Append '[] l = l
+  Append (x : xs) l = x : Append xs l
 
 lemAppendNil :: Append a '[] :~: a
 lemAppendNil = unsafeCoerce Refl
-- 
cgit v1.2.3-70-g09d2