Commit 2020-08-15 12:43 658cd387
View on Github →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