mathlib documentation

control.traversable.derive

similar to nested_traverse but for functor

meta def tactic.interactive.map_field (n : name) (cl f α β e : expr) :

similar to traverse_field but for functor

meta def tactic.interactive.map_constructor (c n : name) (f α β : expr) (args₀ : list expr) (args₁ : list (bool × expr)) (rec_call : list expr) :

similar to traverse_constructor but for functor

meta def tactic.interactive.mk_map (type : name) :

derive the map definition of a functor

meta def tactic.interactive.derive_map_equations (pre : option name) (n : name) (vs : list expr) (tgt : expr) :

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 (n : name) (appl_inst cl f v e : 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 (c n : name) (appl_inst f α β : expr) (args₀ : list expr) (args₁ : list (bool × expr)) (rec_call : list 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 (n cls : name) (tac : tactic unit) (namesp : option name) (mk_inst : nameexprtactic expr := λ (n : name) (arg : expr), (tactic.mk_app n [arg])) :
meta def tactic.interactive.higher_order_derive_handler (cls : name) (tac : tactic unit) (deps : list derive_handler := list.nil) (namesp : option name) (mk_inst : nameexprtactic expr := λ (n : name) (arg : expr), (tactic.mk_app n [arg])) :