The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Stijn Timbermont wrote:
> Concretely, I want to encode something that on paper would be written as 
> follows
>
> A ::=  0  |  A1 U A2  |  X  |  [A]  |  A \ X
>
> [...]
>
> Then I tried using Ensembles, and prove the laws.
> A is then defined as Ensemble Aelt, so I have to define the element type.
> The problem then is the form [A].
>
> Require Import Ensembles.
>
> Definition X := nat.
>
> Inductive Aelt : Type :=
>   | e_single : X ->  Aelt
>   | a_encap  : Ensemble Aelt ->  Aelt.
>
> This last definition is rejected with "Non-strictly positive
> occurrence of "Aelt" in "Ensemble Aelt ->  Aelt".
>    

Can you explain why you need an inductive type of sets and elements?  
Why not assign different Coq types to X's, sets of X's, sets of sets of 
X's, and so on?