mathlib documentation

control.traversable.derive

meta def tactic.interactive.with_prefix :

option name → name → name

meta def tactic.interactive.nested_map (f v : expr) :

expr → tactic expr

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.mk_mapp_aux' :

expr → expr → list expr → tactic expr

meta def tactic.interactive.mk_mapp' (fn : expr) (args : list expr) :

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

meta def tactic.interactive.derive_functor (pre : option name) :

meta def tactic.interactive.nested_traverse (f v : expr) :

expr → tactic expr

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) :

tactic (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 (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.

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

derive the traverse definition of a traversable instance

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

derive the equations for a specific traverse definition

meta def tactic.interactive.derive_traverse (pre : option name) :

meta def tactic.interactive.mk_one_instance (n cls : name) (tac : tactic unit) (namesp : option name) (mk_inst : name → expr → tactic expr := λ (n : name) (arg : expr), (tactic.mk_app n [arg])) :

meta def tactic.interactive.get_equations_of (n : name) :

tactic (list pexpr)

meta def tactic.interactive.derive_lawful_functor (pre : option name) :

meta def tactic.interactive.simp_functor (rs : list tactic.simp_arg_type := list.nil) :

meta def tactic.interactive.traversable_law_starter (rs : list tactic.simp_arg_type) :

meta def tactic.interactive.derive_lawful_traversable (pre : option name) :

meta def tactic.interactive.guard_class (cls : name) (hdl : derive_handler) :

meta def tactic.interactive.higher_order_derive_handler (cls : name) (tac : tactic unit) (deps : list derive_handler := list.nil) (namesp : option name) (mk_inst : name → expr → tactic expr := λ (n : name) (arg : expr), (tactic.mk_app n [arg])) :

meta def tactic.interactive.functor_derive_handler' (nspace : option name := none) :

meta def tactic.interactive.functor_derive_handler :

meta def tactic.interactive.traversable_derive_handler' (nspace : option name := none) :

meta def tactic.interactive.traversable_derive_handler :

meta def tactic.interactive.lawful_functor_derive_handler' (nspace : option name := none) :

meta def tactic.interactive.lawful_functor_derive_handler :

meta def tactic.interactive.lawful_traversable_derive_handler' (nspace : option name := none) :

meta def tactic.interactive.lawful_traversable_derive_handler :