blob: ace1de45daa72453d108b21f195380faa583e29b (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
{-# LANGUAGE TypeFamilies, TypeOperators, GADTs, RankNTypes, FlexibleContexts #-}
module Equality( (:=:), eq_elim, eq_refl ) where
data a:=: b where
EQUAL :: a :=: a
eq_refl :: a :=: a
eq_refl = EQUAL
eq_elim :: (a~b) => a :=: b -> (a~b => p) -> p
eq_elim EQUAL p = p
|
