A mechanism for defining tactics for use in auto params, whose meaning is defined incrementally through attributes.
@[foo] meta def foo_1 : tactic unit := ...replaces the current definition of
@[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
noneif this is the first definition tagged with
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.