Stream: Coq users

Topic: Not an arity for Inductive Type

view this post on Zulip 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

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?

view this post on Zulip 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

view this post on Zulip 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