Zulip Chat Archive

Stream: general

Topic: derive


Hans-Dieter Hiep (Feb 13 2019 at 16:36):

With @[derive decidable_eq] one can automatically make the following inductive type an instance of decidable equality. How about automatically deriving inhabitance for inductive types? Is that also possible? Currently, failed to find a derive handler for 'inhabited'.

Edward Ayers (Feb 13 2019 at 16:41):

@[derive X] looks for derive_handler with the @[derive_handler] attribute on it and then uses that tactic to derive stuff. Afaik nobody has made one for inhabited but you can write your own in Lean.

Edward Ayers (Feb 13 2019 at 16:42):

Lean core has support for decidable_eq, sizeof, has_reflect.

Edward Ayers (Feb 13 2019 at 16:43):

@Simon Hudon wrote some in mathlib for category theory.

Edward Ayers (Feb 13 2019 at 16:44):

You can see how @[derive decidable_eq] works in library/init/meta/mk_dec_eq_instance.lean.

Edward Ayers (Feb 13 2019 at 16:45):

Something on my todo list is to write a @[derive decidable_lt].

Edward Ayers (Feb 13 2019 at 16:53):

Ah, there's a library/init/meta/mk_inhabited_instance.lean

Edward Ayers (Feb 13 2019 at 16:55):

So this works for me:

@[derive_handler] meta def inhabited_derive_handler :=
instance_derive_handler ``inhabited mk_inhabited_instance

@[derive inhabited]
inductive hello | A | B

@[derive inhabited]
inductive world
| A : string  world

lemma world_inhabited : inhabited world := by apply_instance

Edward Ayers (Feb 13 2019 at 16:56):

I don't know why Leo didn't add the @[derive_handler] for inhabited.

Bryan Gin-ge Chen (Feb 13 2019 at 17:02):

I don't know why Leo didn't add the @[derive_handler] for inhabited.

Maybe this: https://github.com/leanprover/lean/pull/1818#issuecomment-328931432 ?


Last updated: Dec 20 2023 at 11:08 UTC