tactic.transform_decl

meta def tactic.copy_attribute' (attr_name src tgt : name) (p : option bool := option.none) :

copy_attribute' attr_name src tgt p d_name copy (user) attribute attr_name from src to tgt if it is defined for src; unlike copy_attribute the primed version also copies the parameter of the user attribute, in the user attribute case. Make it persistent if p is tt; if p is none, the copied attribute is made persistent iff it is persistent on src

source

meta def tactic.additive_test_aux (f : name → option name) (ignore : name_map (list ℕ)) :

bool → expr → bool

Auxilliary function for additive_test. The bool argument only matters when applied to exactly a constant.

source

meta def tactic.additive_test (f : name → option name) (replace_all : bool) (ignore : name_map (list ℕ)) (e : expr) :

bool

additive_test f replace_all ignore e tests whether the expression e contains no constant nm that is not applied to any arguments, and such that f nm = none. This is used in @[to_additive] for deciding which subexpressions to transform: we only transform constants if additive_test applied to their first argument returns tt. This means we will replace expression applied to e.g. α or α × β, but not when applied to e.g. ℕ or ℝ × α. f is the dictionary of declarations that are in the to_additive dictionary. We ignore all arguments specified in the name_map ignore. If replace_all is tt the test always return tt.

source

meta def tactic.transform_decl_with_prefix_fun_aux (f : name → option name) (replace_all trace : bool) (relevant : name_map ℕ) (ignore reorder : name_map (list ℕ)) (pre tgt_pre : name) :

name → tactic unit

transform the declaration src and all declarations pre._proof_i occurring in src using the dictionary f. replace_all, trace, ignore and reorder are configuration options. pre is the declaration that got the @[to_additive] attribute and tgt_pre is the target of this declaration.

source

meta def tactic.transform_decl_with_prefix_fun (f : name → option name) (replace_all trace : bool) (relevant : name_map ℕ) (ignore reorder : name_map (list ℕ)) (src tgt : name) (attrs : list name) :

tactic unit

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the function f. This is used to implement @[to_additive].

source

meta def tactic.transform_decl_with_prefix_dict (dict : name_map name) (replace_all trace : bool) (relevant : name_map ℕ) (ignore reorder : name_map (list ℕ)) (src tgt : name) (attrs : list name) :

tactic unit

Make a new copy of a declaration, replacing fragments of the names of identifiers in the type and the body using the dictionary dict. This is used to implement @[to_additive].