blob: cb621554cb241094bd660e11273c8060fde59e13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
{-# 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
lemAppendNil :: Append a '[] :~: a
lemAppendNil = unsafeCoerce Refl
lemAppendAssoc :: Append a (Append b c) :~: Append (Append a b) c
lemAppendAssoc = unsafeCoerce Refl
|
