blob: 7dbf680dd07fd45ebf753e914a8a19c9fc67665e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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
|
