The Coq mailing list

[Cuihtlauac ALVARADO <cuihtlauac.alvarado AT francetelecom.com>]

> > What's so bad about K anyway?
> >
> >Dependent pattern matching is currently difficult in Coq, but it doesn't
> >have to be that way. The question is what to do about it.
> >
> >On conna\^it la chanson...
> >
> I don't have anything in particular agains K, but in general I don't 
> like axioms. When you are forced to use an axiom it means that your type 
> theory is not doing the job. One should rather rething the system so 
> that the desired properties are "structural" rather that axiomatic.
> In the case under study, Pierre Casteran showed how to do things without 
> assuming axioms, if you can do without them you should.
> A part from this philosophical point, I have no objection: go ahead and 
> use K!

On the other hand you can prove K for (vect A) if equality over A is
decidable, which happens, sometimes :-)

-- 
Cuihtlauac ALVARADO - France Telecom - R&D - +33296053273
2, av Pierre Marzin - 22307 Lannion - France