Type decidable_eq

Stream: new members

[Chase Norman]

I am looking to prove ‘decidable_eq’ for a structure like this for the purpose of program verification:
structure graph := (V : Type) (f : fintype V) (d : decidable_eq V) (w : V → V → ℤ)
It has become clear that this graph does not satisfy decidable_eq because Type does not satisfy decidable_eq. I would like to have different graphs of different types. Is there some subtype of Type that I should use that has decidable equality? And how would I go about proving decidable equality of the resulting ‘graph’ type?

[Mario Carneiro]

you should move V to a parameter

[Mario Carneiro]

also probably [fintype V] [decidable_eq V]

[Chase Norman]

How might you place multiple graph instances with different V in the same list, for instance? @Mario Carneiro

[Chase Norman]

It is actually my intention that the node type V is compared when two graphs are compared. However, since Type does not have decidable equality, it seems that I will need to choose a subtype.

[Mario Carneiro]

In general, you can't do this because different types can't be compared. (#xy ?) For an enumerated list or schema of types, you can do it by having an inductive type (with decidable equality) giving the schema, and then an evaluation function which gives the type for one representative in order to put a graph structure on it