[Agda] Data.Vec.Equality.PropositionalEquality should publish _\~=_

Helmut Grohne helmut at subdivi.de
Wed Sep 5 18:32:10 CEST 2012


Hi,

< copumpkin> helmut: opening propositional equality should work
< copumpkin> oh wait
< copumpkin> it doesn't open it publicly
< copumpkin> that's just a bug
< copumpkin> but you can open Equality yourself with P.setoid

So as I created a patch for this issue and attached it.

Please CC me in a reply, as I am not subscribed.

Helmut
-------------- next part --------------
A non-text attachment was scrubbed...
Name: agda-lib.patch
Type: text/x-diff
Size: 7654 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20120905/188c43e4/agda-lib.bin


More information about the Agda mailing list