mathlib documentation

control.traversable.derive

similar to nested_traverse but for functor

meta def tactic.interactive.map_field  :
nameexprexprexprexprexprtactic expr

similar to traverse_field but for functor

meta def tactic.interactive.map_constructor  :
namenameexprexprexprlist exprlist (bool × expr)list exprtactic expr

similar to traverse_constructor but for functor

derive the map definition of a functor

derive the equations for a specific map definition

nested_traverse f α (list (array n (list α))) synthesizes the expression traverse (traverse (traverse f)). nested_traverse assumes that α appears in (list (array n (list α)))

meta def tactic.interactive.traverse_field  :
nameexprexprexprexprexprtactic (expr expr)

For a sum type inductive foo (α : Type) | foo1 : list α → ℕ → foo | ... traverse_field `foo appl_inst f `α `(x : list α) synthesizes traverse f x as part of traversing foo1.

meta def tactic.interactive.traverse_constructor  :
namenameexprexprexprexprlist exprlist (bool × expr)list exprtactic expr

For a sum type inductive foo (α : Type) | foo1 : list α → ℕ → foo | ... traverse_constructor `foo1 `foo appl_inst f `α `β [`(x : list α), `(y : ℕ)] synthesizes foo1 <$> traverse f x <*> pure y.

derive the traverse definition of a traversable instance

derive the equations for a specific traverse definition

meta def tactic.interactive.mk_one_instance  :
namenametactic unitoption name(nameexprtactic expr := λ (n : name) (arg : expr), (tactic.mk_app n [arg]))tactic unit