coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Helmut Brandl <helmut.brandl AT gmx.net>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Dependent Functional Extensionality
- Date: Mon, 23 Oct 2017 17:08:02 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
- Ironport-phdr: 9a23:qQPoFR8WThAFff9uRHKM819IXTAuvvDOBiVQ1KB+1uIcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS46tL2HV93a19HsZHgj1HQtzPOX8XIDI3Oqt0OXn25DXZhhUzBCnaLV+KF3irQjVs9QKx4F4I6A9zjPGp2sOfelKkzA7bWmPlgrxs5/jtKVo9D5d7qos
In the standard library of Coq there is an axiom for dependent functional extensionality which can be imported on demand (Coq.Logic.FunctionalExtensionality.html).
I was wondering why the type of the functions has been chosen to be forall a:A, A -> B a instead of forall a:A, B a i.e. the usual dependent product.
Is there any reason to state the axiom with the more complicated type. In my opinion the simpler type should be sufficient.
Regards
Helmut
- [Coq-Club] Dependent Functional Extensionality, Helmut Brandl, 10/24/2017
- Re: [Coq-Club] Dependent Functional Extensionality, Helmut Brandl, 10/24/2017
Archive powered by MHonArc 2.6.18.