CODEWITHSUNDEEP
coq
frafle
frafle

Reputation: 25

How to use finite sets represented as lists in attributes of a class in Coq?

I'm using ListSet extension from the standard library of Coq, to use finite sets as attributes of a class: 

Require Import ListSet.
Class aux := {
  attribute1: set;
  attribute2: set -> set;
  }.

but I'm getting this error:

Error: In environment
aux : Type
The term "set" has type "Type -> Type" which should be Set, Prop or Type.

I don't understand why this is happening. (I'm new to Coq)

Upvotes: 0

Views: 108

Answers (1)

Théo Winterhalter
Théo Winterhalter

Reputation: 5108

Coq is telling you that set is not a type but instead of type Type -> Type meaning it takes a type as argument.

If you look at the definition: https://coq.inria.fr/library/Coq.Lists.ListSet.html you can see that it indeed requires a parameter. So the type you want to consider is set A for some type A and in fact it is just the type list A, what the ListSet module brings, are operations on set A that preserve invariants such as the fact that you don't have twice the same element.

Perhaps these are not the sets you had in mind.

Upvotes: 1

Related Questions