Where is `deriving Fintype` defined?

Stream: new members

[Michael Fishman]

I want to understand how deriving Fintype creates elems and complete.

How can I find that code?

More generally, for any class, how can I find the code that defines what happens when we deriving that class?

[Matthew Ballard]

docs#Lean.Elab.elabDeriving is a good plan to start pulling

[Michael Fishman]

Thanks!

[Kyle Miller]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/DeriveFintype.lean

[Kyle Miller]

It uses docs#Fintype.ofEquiv with the proxy_equiv% elaborator (see the imports).

[Kyle Miller]

This is the main code. The next function is just to make an efficient Fintype instance with a known-at-compile-time list of all elements for "enum" inductive types (types whose constructors all have no arguments).