similar to nested_traverse but for functor

similar to traverse_field but for functor

similar to traverse_constructor but for functor

derive the map definition of a functor

derive the equations for a specific map definition

seq_apply_constructor f [x,y,z] synthesizes f <*> x <*> y <*> z

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

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.

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