The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Petar,

in this case it might be easier to use a set type or duplication free list 
type. In my experience it is much more pain to carry along the witnesses in 
dependent types than to use types which have the desired properties by 
construction.

Unfortunately the set types in the standard library are implemented with 
modules and are not first class polymorphic, but if lists are performance 
wise ok as set representation for you, it is easy to define. If not, I would 
be interested to work together on porting relevant standard libraries (tree 
based sets) to type class based first class polymorphic implementations.

Best regards,

Michael


-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Petar Maksimovic
Sent: Thursday, October 01, 2015 4:14 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Records and Inductive definitions

Thanks Pierre-Marie and Epiphanie,

Vectors would work if my example hadn't been somewhat under-illustrative. 
What I would really like is

Record list_noDup (T : Type) := {lT :> list T; cond: noDup lT}.

Inductive T : Type :=
 | T_main : list_noDup T -> T.

but for that I think I'll need some sort of workaround.

Cheers,
Petar
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928