Instead of the usual Ensemble, I was trying to implement Sets of nats as lists of nats. For this, I would need to specify the list os nats as the arity of an inductively defined propositions as follows:

```
Fixpoint In (l:natlist) (a:nat) : Prop :=
match l with
| [] => False
| b :: m => b = a \/ In m a
end.
Inductive Intersection (B C: natlist) : natlist :=
Intersection_intro :
forall x:nat, (++ In B x) -> (++ In C x) -> In (Intersection B C) x.
```

But I get the message `Not an arity`

when I try to run the definition of `Intersection`

. Why does this happen? Is there any solution to continue in this approach of implementation?

it means an inductive type should have a type of the form `some stuff -> Type`

`natlist`

doesn't fit that pattern

Implementing nat sets as nat lists is fine, and so is your definition of In. But Intersection : natlist -> natlist-> natlist must be a function.

Last updated: Oct 04 2023 at 21:01 UTC