mathlibdocumentation

tactic.transform_decl

meta def tactic.additive_test_aux (f : name) (ignore : name_map (list )) :
bool

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

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

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.

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

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

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

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