mathlib 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.

meta def tactic.inhabited_instance :

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]

def tactic.apply_cfg.inhabited :

inhabited tactic.apply_cfg

@[protected, instance]

def tactic_doc_entry.inhabited :

inhabited tactic_doc_entry

@[protected, instance]

def interactive.loc.inhabited :

inhabited interactive.loc

@[protected, instance]

def pos.inhabited :

@[protected, instance]

def smt_pre_config.inhabited :

inhabited smt_pre_config

@[protected, instance]

def reducibility_hints.inhabited :

inhabited reducibility_hints

@[protected, instance]

def environment.projection_info.inhabited :

inhabited environment.projection_info

@[protected, instance]

def tactic.unfold_proj_config.inhabited :

inhabited tactic.unfold_proj_config

@[protected, instance]

def vm_decl_kind.inhabited :

inhabited vm_decl_kind

@[protected, instance]

def rsimp.config.inhabited :

inhabited rsimp.config

@[protected, instance]

def ulift.inhabited (α : Type s) [a : inhabited α] :

inhabited (ulift α)

@[protected, instance]

def tactic.simp_config.inhabited :

inhabited tactic.simp_config

@[protected, instance]

def tactic.transparency.inhabited :

inhabited tactic.transparency

@[protected, instance]

def tactic.rewrite_cfg.inhabited :

inhabited tactic.rewrite_cfg

@[protected, instance]

def tactic.new_goals.inhabited :

inhabited tactic.new_goals

@[protected, instance]

def format.color.inhabited :

inhabited format.color

@[protected, instance]

def tactic.delta_config.inhabited :

inhabited tactic.delta_config

@[protected, instance]

def subsingleton_info.inhabited :

inhabited subsingleton_info

@[protected, instance]

def rbnode.color.inhabited :

inhabited rbnode.color

@[protected, instance]

def tactic.dsimp_config.inhabited :

inhabited tactic.dsimp_config

@[protected, instance]

def smt_config.inhabited :

inhabited smt_config

@[protected, instance]

def congr_arg_kind.inhabited :

inhabited congr_arg_kind

@[protected, instance]

def unification_constraint.inhabited :

inhabited unification_constraint

@[protected, instance]

def unification_hint.inhabited :

inhabited unification_hint

@[protected, instance]

def pprod.inhabited (α : Sort u) [a : inhabited α] (β : Sort v) [a_1 : inhabited β] :

inhabited (pprod α β)

@[protected, instance]

def fun_info.inhabited :

inhabited fun_info

@[protected, instance]

def tactic.dunfold_config.inhabited :

inhabited tactic.dunfold_config

@[protected, instance]

def cc_config.inhabited :

inhabited cc_config

@[protected, instance]

def doc_category.inhabited :

inhabited doc_category

@[protected, instance]

def ematch_config.inhabited :

inhabited ematch_config

@[protected, instance]

def param_info.inhabited :

inhabited param_info

@[protected, instance]

def plift.inhabited (α : Sort u) [a : inhabited α] :

inhabited (plift α)

@[protected, instance]

def string_imp.inhabited :

inhabited string_imp

@[protected, instance]

def ordering.inhabited :

inhabited ordering

@[protected, instance]

def tactic.unfold_config.inhabited :

inhabited tactic.unfold_config

@[protected, instance]

def tactic.simp_intros_config.inhabited :

inhabited tactic.simp_intros_config

@[protected, instance]

def string.iterator_imp.inhabited :

inhabited string.iterator_imp

@[protected, instance]

def vm_obj_kind.inhabited :

inhabited vm_obj_kind

@[protected, instance]

def bin_tree.inhabited {α : Type u_1} :

inhabited (bin_tree α)

Equations

bin_tree.inhabited = {default := bin_tree.empty α}

@[protected, instance]

def unsigned.inhabited :

inhabited unsigned

Equations

unsigned.inhabited = {default := 0}

@[protected, instance]

def string.iterator.inhabited :

inhabited string.iterator

Equations

string.iterator.inhabited = string.iterator_imp.inhabited

@[protected, instance]

def rbnode.inhabited {α : Type u_1} :

inhabited (rbnode α)

Equations

rbnode.inhabited = {default := rbnode.leaf α}

@[protected, instance]

def rbtree.inhabited {α : Type u_1} {lt : α → α → Prop . "default_lt"} :

inhabited (rbtree α lt)

Equations

rbtree.inhabited = {default := mk_rbtree α lt}

@[protected, instance]

def rbmap.inhabited {α : Type u_1} {β : Type u_2} {lt : α → α → Prop . "default_lt"} :

inhabited (rbmap α β lt)

Equations

rbmap.inhabited = {default := mk_rbmap α β lt}