[Agda] [PATCH] add a ∷-injective for Vec like there is one for List

[Andreas Abel]

Recorded an pushed to github.  -- Thx, Andreas

On 17.01.2014 12:25, Helmut Grohne wrote:
> Hi,
>
> I found myself in need of injectivity of Vec._∷_ in a few places. While
> there is a ∷-injective for List, there is none for Vec yet. I attach a
> simple patch (in a format suitable to git am) to address this omission
> and license it under the MIT license used for the standard library. I'd
> appreciate if it could be merged. Thanks.
>
> Helmut
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/