[Agda] Fin n -> Fin n extensional?

João Paulo Pizani Flor J.P.PizaniFlor at uu.nl
Wed Feb 18 16:47:55 CET 2015


Not yet (couldn't find it anywhere), but I will probably need it for my
Ph.D project, so maybe it will come in some time...

Cheers,

João Pizani, M.Sc <j.p.pizaniflor at uu.nl>
Promovendus - Departement Informatica
Faculteit Bètawetenschappen - Universiteit Utrecht

On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette <carette at mcmaster.ca>
wrote:

> Does anyone have a proof in Agda that functions at type (Fin n -> Fin n)
> are extensional?
> Jacques
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150218/e56ee70a/attachment.html


More information about the Agda mailing list