2009/3/17 Luke Palmer <[email protected]>:
>> Here are the original definition and the proofs of comm and trans.
>> Compiles
>> fine with GHC 6.10.1.
>>
>> data (a :=: a') where
>>
>> Refl :: a :=: a
>>
>> comm :: (a :=: a') -> (a' :=: a)
>> comm Refl = Refl
>>
>> trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')
>> trans Refl Refl = Refl
>
> These two theorems should be in the package.
How about this?
instance Category (:=:) where
id = Refl
Refl . Refl = Refl
--
Dave Menendez <[email protected]>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
