derive

Stream: general

[Hans-Dieter Hiep]

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]

@[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]

Lean core has support for decidable_eq, sizeof, has_reflect.

[Edward Ayers]

@Simon Hudon wrote some in mathlib for category theory.

[Edward Ayers]

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

[Edward Ayers]

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

[Edward Ayers]

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

[Edward Ayers]

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]

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

[Bryan Gin-ge Chen]

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 ?