Enum/fintype/encodable deriving handler

Stream: Is there code for X?

[nrs]

Has anyone ever encountered/worked on/tinkered with making deriving handlers for enum-like types such as inductive myEnum | a | b | c that would give a cardinality and a decidable ordering? If there are no such examples, what handlers would you consider useful having? (e.g. there is more than one possible choice for the type of a finite collection)

[Edward van de Meent]

i think there already is an Encodable deriver in mathlib...

[Edward van de Meent]

probably same for Fintype

[Edward van de Meent]

yup

[Edward van de Meent]

import Mathlib.Tactic.DeriveFintype
import Mathlib.Tactic.DeriveEncodable

inductive Foo
| a
| b
| c
deriving Fintype, Encodable

[nrs]

very cool! thank you!!

[Kyle Miller]

I was going to say, if you did import Mathlib, you could have tried it already and experienced the pleasant surprise sooner :wink:

[Kyle Miller]

There's also a Countable handler, in case you have a parameterized type whose parameters might only be Countable.

[nrs]

thanks for the reference! I got discouraged after not seeing them in the manual heheh

[Kyle Miller]

Want to make a contribution to it @nrs? I'm happy to answer questions about these handlers and their limitations.

[nrs]

Sure, how do we manage the mentions of mathlib in the manual?

[Kyle Miller]

I suppose it depends on which manual you're talking about then. Neither Fintype nor Encodable are in core Lean, so not seeing any mention of deriving handlers for them in the Lean language reference manual doesn't mean anything.

[nrs]

Oh I actually didn't know there is also a mathlib manual lol!

[Edward van de Meent]

there isn't

[nrs]

there's this fork I just now discovered https://github.com/leanprover-community/mathlib-manual, no clue how official it is

[Edward van de Meent]

:looking: it looks like it's at least somewhat official, seeing as it is in the leanprover-community group?

[Kyle Miller]

Yes, https://leanprover-community.github.io/mathlib-manual/html-multi/ is very new. It would be a good place to document the Mathlib deriving handlers.

[Kyle Miller]

(Thanks @Jon Eugster for getting this going!)

[Jon Eugster]

if people actively PR content, it could become more and more official :)

I can help if you need help getting a grip with the verso syntax, just DM me

[nrs]

There's currently section 1.Tactics, would we have section 2. Deriving handlers? Or maybe it would make sense to have deriving handlers as a subsection their specific type

[Jon Eugster]

I don't mind, having 2. Deriving handlers sounds reasonable.