coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Victor Porton <porton AT narod.ru>
- Cc: coq-club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] A false hope: A thing which cannot be directly expressed in Coq
- Date: Sat, 29 Dec 2012 12:42:26 -0500
On 12/29/2012 12:36 PM, Victor Porton wrote:
Intuitively this formula is clear. It expresses an equality for arbitrary
objects A, B, C.
But when we write it explicitly, we need to add before it:
forall A, B, C, f in Hom(A;B), g in Hom(B;C), h in Hom(A;C).
This is cumbersome as possibly objects for f, g, h can be inferred from the
formula itself (which intuitively implies that f and g have the same source
and destination, that the source of h is the same as the source of f etc.)
and to specify it explicitly is too cumbersome.
General type inference for Coq is undecidable, so there is no obvious way of inferring "extra" implicit quantifiers in all situations. Personally, I prefer to write the quantifiers out manually, rather than understand some heuristic which could in theory be added to Coq.
- [Coq-Club] A false hope: A thing which cannot be directly expressed in Coq, Victor Porton, 12/29/2012
- Re: [Coq-Club] A false hope: A thing which cannot be directly expressed in Coq, Adam Chlipala, 12/29/2012
- Re: [Coq-Club] A false hope: A thing which cannot be directly expressed in Coq, Kristopher Micinski, 12/29/2012
Archive powered by MHonArc 2.6.18.