Derive handler for inhabited instances
This file introduces a derive handler to automatically generate inhabited
instances for structures and inductives. We also add various inhabited
instances for types in the core library.
Tries to derive an inhabited instance for inductives and structures.
For example:
@[derive inhabited]
structure foo :=
(a : ℕ := 42)
(b : list ℕ)
Here, @[derive inhabited] adds the instance foo.inhabited, which is defined as
⟨⟨42, default (list ℕ)⟩⟩. For inductives, the default value is the first constructor.
If the structure/inductive has a type parameter α, then the generated instance will have an
argument inhabited α, even if it is not used. (This is due to the implementation using
instance_derive_handler.)
@[instance]
Equations
@[instance]
Equations
- unsigned.inhabited = {default := 0}
@[instance]
Equations
- string.iterator.inhabited = string.iterator_imp.inhabited
@[instance]
Equations
- rbnode.inhabited = {default := rbnode.leaf α}
@[instance]
Equations
- rbtree.inhabited = {default := mk_rbtree α lt}
@[instance]
Equations
- rbmap.inhabited = {default := mk_rbmap α β lt}