The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Op woensdag 24-03-2010 om 11:45 uur [tijdzone -0400], schreef Ruddy
Hahn:
> I am interested in representing lists of natural numbers without
> repetition of occurrences, using inductive types. 

This is used as a standard example for induction-recursion, which Coq
does not support directly.

See, for example, this paper by Venanzio Capretta on a representation of
induction-recursion in the Calculus of Inductive Constructions:
http://www.cs.ru.nl/~venanzio/publications/induction_recursion.pdf