The Coq mailing list

[Vladimir Voevodsky <(e6fa90e88c%hidden_head%e6fa90e88c)vladimir(e6fa90e88c%hidden_at%e6fa90e88c)ias.edu(e6fa90e88c%hidden_end%e6fa90e88c)>]

In my opinion the type "Set" in Coq is redundant.  So if you plan to develop 
such a library it is much more useful to do it for Type.

Vladimir. 






On Dec 9, 2009, at 10:46 AM, Christian Doczkal wrote:

> Hello
> 
> I'm planning some development with uses sets in various places and my
> (preliminary) experience is that the Sets libraries that ship with Coq
> are somewhat cumbersome to work with. 
> 
> Has anyone used this for some (larger) development? I'm not overly
> worried about having to assume classical logic and various
> extensionality axioms. I'm more interested in increased automation for
> the set reasoning part.
> 
> The tactic "eauto with sets" only works in relatively few cases, even
> after including Finete_sets_faacts which in turn exports almost about
> the whole library on sets.
> 
> (Notation is also not an issue, this I have taken care of)
> 
> -- 
> Regards
> Christian Doczkal
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club