blob: 55ef042daaab718da787c8c9c8ebdb8db8874478 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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
|
