mathlib3 documentation

tactic.replacer

def_replacer #

A mechanism for defining tactics for use in auto params, whose meaning is defined incrementally through attributes.

meta def tactic.replacer_core {α : Type} [reflected Type α] (ntac : name) (eval : Π (β : Type) [_inst_2 : reflected Type β], expr tactic β) :
meta def tactic.replacer (ntac : name) {α : Type} [reflected Type α] (F : Type Type) (eF : Π (β : Type), reflected Type β reflected Type (F β)) (R : Π (β : Type), F β β) :
meta def tactic.mk_replacer (ntac : name) (e : expr) :
meta def tactic.def_replacer (ntac : name) (ty : expr) :

Define a new replaceable tactic.

def_replacer foo sets up a stub definition foo : tactic unit, which can effectively be defined and re-defined later, by tagging definitions with @[foo].

  • @[foo] meta def foo_1 : tactic unit := ... replaces the current definition of foo.
  • @[foo] meta def foo_2 (old : tactic unit) : tactic unit := ... replaces the current definition of foo, and provides access to the previous definition via old. (The argument can also be an option (tactic unit), which is provided as none if this is the first definition tagged with @[foo] since def_replacer was invoked.)

def_replacer foo : α → β → tactic γ allows the specification of a replacer with custom input and output types. In this case all subsequent redefinitions must have the same type, or the type α → β → tactic γ → tactic γ or α → β → option (tactic γ) → tactic γ analogously to the previous cases.

def_replacer foo sets up a stub definition foo : tactic unit, which can effectively be defined and re-defined later, by tagging definitions with @[foo].

  • @[foo] meta def foo_1 : tactic unit := ... replaces the current definition of foo.
  • @[foo] meta def foo_2 (old : tactic unit) : tactic unit := ... replaces the current definition of foo, and provides access to the previous definition via old. (The argument can also be an option (tactic unit), which is provided as none if this is the first definition tagged with @[foo] since def_replacer was invoked.)

def_replacer foo : α → β → tactic γ allows the specification of a replacer with custom input and output types. In this case all subsequent redefinitions must have the same type, or the type α → β → tactic γ → tactic γ or α → β → option (tactic γ) → tactic γ analogously to the previous cases.