mathlib documentation

tactic.replacer

def_replacer #

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

source
meta def tactic.replacer_core {α : Type} [reflected Type α] (ntac : name) (eval : Π (β : Type) [_inst_2 : reflected Type β], expr → tactic β) :
list name → tactic α
source
meta def tactic.replacer (ntac : name) {α : Type} [reflected Type α] (F : Type → Type) (eF : Π (β : Type), reflected Type β → reflected Type (F β)) (R : Π (β : Type), F β → β) :
tactic α
source
meta def tactic.mk_replacer₁  :
expr → ℕ → expr × expr
source
meta def tactic.mk_replacer₂ (ntac : name) (v : expr × expr) :
expr → ℕ → option expr
source
meta def tactic.mk_replacer (ntac : name) (e : expr) :
tactic expr
source
meta def tactic.valid_types  :
expr → list expr
source
meta def tactic.replacer_attr (ntac : name) :
(user_attribute unit)
source
meta def tactic.def_replacer (ntac : name) (ty : expr) :
tactic unit

Define a new replaceable tactic.

source
meta def tactic.def_replacer_cmd (_x : interactive.parse (lean.parser.tk "def_replacer")) :
lean.parser unit

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.

source
def tactic_doc.command.def_replacer  :
tactic_doc_entry

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.

source
meta def tactic.unprime  :
name → tactic name
source
meta def tactic.replaceable_attr  :
(user_attribute unit)