Commit 2020-08-15 12:43 658cd387

feat(tactic/derive_fintype): derive fintype instances (#3772) This adds a @[derive fintype] implementation, like so:

@[derive fintype]
inductive foo (α : Type)
| A : α → foo
| B : α → α → foo
| C : α × α → foo
| D : foo