mathlib3 documentation

tactic.derive_inhabited

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⟩⟩. 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.)

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def ulift.inhabited (α : Type s) [a : inhabited α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def pprod.inhabited (α : Sort u) [a : inhabited α] (β : Sort v) [a_1 : inhabited β] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def plift.inhabited (α : Sort u) [a : inhabited α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def bin_tree.inhabited {α : Type u_1} :
Equations
@[protected, instance]
Equations
@[protected, instance]
def rbnode.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def rbtree.inhabited {α : Type u_1} {lt : α α Prop . "default_lt"} :
Equations
@[protected, instance]
def rbmap.inhabited {α : Type u_1} {β : Type u_2} {lt : α α Prop . "default_lt"} :
inhabited (rbmap α β lt)
Equations