fintype from enumerated type

Stream: general

[Jeremy Avigad]

Is there a canonical idiom for making a fintype from an enumerated type? This is what I came up with:

import data.fintype

@[derive decidable_eq]
inductive foo : Type | a | b | c
open foo

def foo.of_fin : fin 3 → foo
| ⟨1, _⟩ := a
| ⟨2, _⟩ := b
| _     := c

instance : fintype foo :=
fintype.of_surjective foo.of_fin (λ x, foo.cases_on x ⟨1, rfl⟩ ⟨2, rfl⟩ ⟨3, rfl⟩)

I actually want to do something a little more general, namely an inductive type with nonrecursive constructors with arguments from other fintypes. It would be an interesting metaprogramming exercise to build the instance automatically, but not hard to build a surjection by hand in the instance I need.

[Mario Carneiro]

I don't think there is any general solution better than your example

[Mario Carneiro]

The general technique would be to build an equiv to a sum of products of unit or other fintypes