# Documentation

Mathlib.Tactic.DeriveTraversable

# Deriving handler for Traversable instances #

This module gives deriving handlers for Functor, LawfulFunctor, Traversable, and LawfulTraversable. These deriving handlers automatically derive their dependencies, for example deriving LawfulTraversable all by itself gives all four.

nestedMap f α (List (Array (List α))) synthesizes the expression Functor.map (Functor.map (Functor.map f)). nestedMap assumes that α appears in (List (Array (List α))).

(Similar to nestedTraverse but for Functor.)

similar to traverseField but for Functor

Instances For

Get the auxiliary local declaration corresponding to the current declaration. If there are multiple declaraions it will throw.

Instances For
def Mathlib.Deriving.Traversable.mapConstructor (c : Lean.Name) (n : Lean.Name) (f : Lean.Expr) (α : Lean.Expr) (β : Lean.Expr) (args₀ : ) (args₁ : ) (m : Lean.MVarId) :

similar to traverseConstructor but for Functor

Instances For
def Mathlib.Deriving.Traversable.mkCasesOnMatch (type : Lean.Name) (levels : ) (params : ) (motive : Lean.Expr) (indices : ) (val : Lean.Expr) (rhss : ) :

Makes a match expression corresponding to the application of casesOn like:

match (motive := motive) indices₁, indices₂, .., (val : type.{univs} params₁ params₂ ..) with
| _, _, .., ctor₁ fields₁₁ fields₁₂ .. => rhss ctor₁ [fields₁₁, fields₁₂, ..]
| _, _, .., ctor₂ fields₂₁ fields₂₂ .. => rhss ctor₂ [fields₂₁, fields₂₂, ..]


This is convenient to make a definition with equation lemmas.

Instances For

Get FVarIds which is not implementation details in the current context.

Instances For

Get Exprs of FVarIds which is not implementation details in the current context.

Instances For

derive the map definition of a Functor

Instances For

derive the map definition and declare Functor using this.

Instances For

Similar to mkInstanceName, but for a Expr type.

Instances For
def Mathlib.Deriving.Traversable.mkOneInstance (n : Lean.Name) (cls : Lean.Name) (tac : ) (mkInst : optParam () fun n arg => liftM (Lean.Meta.mkAppM n #[arg])) :

Derive the cls instance for the inductive type constructor n using the tac tactic.

Instances For

Make the new deriving handler depends on other deriving handlers.

Instances For

The deriving handler for Functor.

Instances For

Prove the functor laws and derive LawfulFunctor.

Instances For

The deriving handler for LawfulFunctor.

Instances For

nestedTraverse f α (List (Array (List α))) synthesizes the expression traverse (traverse (traverse f)). nestedTraverse assumes that α appears in (List (Array (List α)))

For a sum type inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ... traverseField Foo f α (x : List α) synthesizes traverse f x as part of traversing foo1.

Instances For
def Mathlib.Deriving.Traversable.traverseConstructor (c : Lean.Name) (n : Lean.Name) (applInst : Lean.Expr) (f : Lean.Expr) (α : Lean.Expr) (β : Lean.Expr) (args₀ : ) (args₁ : ) (m : Lean.MVarId) :

For a sum type inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ... traverseConstructor foo1 Foo applInst f α β [(x : List α), (y : ℕ)] synthesizes foo1 <\$> traverse f x <*> pure y.

Instances For
def Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor (c : Lean.Name) (args : ) (fvars : optParam () #[]) (aargs : optParam () #[]) :

mkFunCtor ctor [(true, (arg₁ : m type₁)), (false, (arg₂ : type₂)), (true, (arg₃ : m type₃)), (false, (arg₄ : type₄))] makes fun (x₁ : type₁) (x₃ : type₃) => ctor x₁ arg₂ x₃ arg₄.

Equations
Instances For

derive the traverse definition of a Traversable instance

Instances For

derive the traverse definition and declare Traversable using this.

Instances For

The deriving handler for Traversable.

Instances For
def Mathlib.Deriving.Traversable.simpFunctorGoal (m : Lean.MVarId) (discharge? : ) (simplifyTarget : ) (fvarIdsToSimp : optParam () #[]) (usedSimps : ) :

Simplify the goal m using functor_norm.

Instances For

Run the following tactic:

intros _ .. x
dsimp only [Traversable.traverse, Functor.map]
induction x <;> (the simp tactic corresponding to s) <;> (tac)

Instances For

Prove the traversable laws and derive LawfulTraversable.

Instances For

The deriving handler for LawfulTraversable`.

Instances For