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: Re: [Coq-Club] Dependent Functional Extensionality
- Date: Mon, 23 Oct 2017 17:12:10 -0500
- Authentication-results: mail2-smtp-roc.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:a6UZtRUy/OkoEtK6GuTIf/ZSpULV8LGtZVwlr6E/grcLSJyIuqrYZRGPt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl9+If2wEYrPhey20fqz8tvdeVZmnj24NJN/KBCrsU37rMAQjY8qfqY8zh7Uvj1CYe1QyWdAKleD2RDx+pHjr9ZY7y1Mtqd5pIZ7WqLgcvFgQA==
I have read the documentation wrongly. Forget about the silly question.
Helmut
On Oct 23, 2017, at 17:08, Helmut Brandl <helmut.brandl AT gmx.net> wrote: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.RegardsHelmut
- [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.