Stream: Coq users

Topic: Not an arity for Inductive Type

João Mendes (Apr 22 2023 at 20:35):

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?

Gaëtan Gilbert (Apr 22 2023 at 21:49):

it means an inductive type should have a type of the form some stuff -> Type
natlist doesn't fit that pattern

Paolo Giarrusso (Apr 23 2023 at 06:53):

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