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.

source
meta def tactic.inhabited_instance  :
derive_handler

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

source
@[protected, instance]
def tactic.apply_cfg.inhabited  :
inhabited tactic.apply_cfg
source
@[protected, instance]
def tactic_doc_entry.inhabited  :
inhabited tactic_doc_entry
source
@[protected, instance]
def interactive.loc.inhabited  :
inhabited interactive.loc
source
@[protected, instance]
def pos.inhabited  :
inhabited pos
source
@[protected, instance]
def smt_pre_config.inhabited  :
inhabited smt_pre_config
source
@[protected, instance]
def reducibility_hints.inhabited  :
inhabited reducibility_hints
source
@[protected, instance]
def environment.projection_info.inhabited  :
inhabited environment.projection_info
source
@[protected, instance]
def tactic.unfold_proj_config.inhabited  :
inhabited tactic.unfold_proj_config
source
@[protected, instance]
def vm_decl_kind.inhabited  :
inhabited vm_decl_kind
source
@[protected, instance]
def rsimp.config.inhabited  :
inhabited rsimp.config
source
@[protected, instance]
def ulift.inhabited (α : Type s) [a : inhabited α] :
inhabited (ulift α)
source
@[protected, instance]
def tactic.simp_config.inhabited  :
inhabited tactic.simp_config
source
@[protected, instance]
def tactic.transparency.inhabited  :
inhabited tactic.transparency
source
@[protected, instance]
def tactic.rewrite_cfg.inhabited  :
inhabited tactic.rewrite_cfg
source
@[protected, instance]
def tactic.new_goals.inhabited  :
inhabited tactic.new_goals
source
@[protected, instance]
def format.color.inhabited  :
inhabited format.color
source
@[protected, instance]
def tactic.delta_config.inhabited  :
inhabited tactic.delta_config
source
@[protected, instance]
def subsingleton_info.inhabited  :
inhabited subsingleton_info
source
@[protected, instance]
def rbnode.color.inhabited  :
inhabited rbnode.color
source
@[protected, instance]
def tactic.dsimp_config.inhabited  :
inhabited tactic.dsimp_config
source
@[protected, instance]
def smt_config.inhabited  :
inhabited smt_config
source
@[protected, instance]
def congr_arg_kind.inhabited  :
inhabited congr_arg_kind
source
@[protected, instance]
def unification_constraint.inhabited  :
inhabited unification_constraint
source
@[protected, instance]
def unification_hint.inhabited  :
inhabited unification_hint
source
@[protected, instance]
def pprod.inhabited (α : Sort u) [a : inhabited α] (β : Sort v) [a_1 : inhabited β] :
inhabited (pprod α β)
source
@[protected, instance]
def fun_info.inhabited  :
inhabited fun_info
source
@[protected, instance]
def tactic.dunfold_config.inhabited  :
inhabited tactic.dunfold_config
source
@[protected, instance]
def cc_config.inhabited  :
inhabited cc_config
source
@[protected, instance]
def doc_category.inhabited  :
inhabited doc_category
source
@[protected, instance]
def ematch_config.inhabited  :
inhabited ematch_config
source
@[protected, instance]
def param_info.inhabited  :
inhabited param_info
source
@[protected, instance]
def plift.inhabited (α : Sort u) [a : inhabited α] :
inhabited (plift α)
source
@[protected, instance]
def string_imp.inhabited  :
inhabited string_imp
source
@[protected, instance]
def ordering.inhabited  :
inhabited ordering
source
@[protected, instance]
def tactic.unfold_config.inhabited  :
inhabited tactic.unfold_config
source
@[protected, instance]
def tactic.simp_intros_config.inhabited  :
inhabited tactic.simp_intros_config
source
@[protected, instance]
def string.iterator_imp.inhabited  :
inhabited string.iterator_imp
source
@[protected, instance]
def vm_obj_kind.inhabited  :
inhabited vm_obj_kind
source
@[protected, instance]
def bin_tree.inhabited {α : Type u_1} :
inhabited (bin_tree α)
Equations
source
@[protected, instance]
def unsigned.inhabited  :
inhabited unsigned
Equations
source
@[protected, instance]
def string.iterator.inhabited  :
inhabited string.iterator
Equations
source
@[protected, instance]
def rbnode.inhabited {α : Type u_1} :
inhabited (rbnode α)
Equations
source
@[protected, instance]
def rbtree.inhabited {α : Type u_1} {lt : α → α → Prop . "default_lt"} :
inhabited (rbtree α lt)
Equations
source
@[protected, instance]
def rbmap.inhabited {α : Type u_1} {β : Type u_2} {lt : α → α → Prop . "default_lt"} :
inhabited (rbmap α β lt)
Equations