# 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.

source
partial def Mathlib.Deriving.Traversable.nestedMap (f v t : Lean.Expr) :
Lean.Elab.TermElabM Lean.Expr

`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`.)

source
def Mathlib.Deriving.Traversable.mapField (n : Lean.Name) (cl f α β e : Lean.Expr) :
Lean.Elab.TermElabM Lean.Expr

similar to `traverseField` but for `Functor`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.getAuxDefOfDeclName :
Lean.Elab.TermElabM Lean.FVarId

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.mapConstructor (c n : Lean.Name) (f α β : Lean.Expr) (args₀ : List Lean.Expr) (args₁ : List (Bool × Lean.Expr)) (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

similar to `traverseConstructor` but for `Functor`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.mkCasesOnMatch (type : Lean.Name) (levels : List Lean.Level) (params : List Lean.Expr) (motive : Lean.Expr) (indices : List Lean.Expr) (val : Lean.Expr) (rhss : Lean.Name → List Lean.FVarId → Lean.Elab.TermElabM Lean.Expr) :
Lean.Elab.TermElabM Lean.Expr

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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.getFVarIdsNotImplementationDetails :
Lean.MetaM (List Lean.FVarId)

Get `FVarId`s which is not implementation details in the current context.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.getFVarsNotImplementationDetails :
Lean.MetaM (List Lean.Expr)

Get `Expr`s of `FVarId`s which is not implementation details in the current context.

Equations

- Mathlib.Deriving.Traversable.getFVarsNotImplementationDetails = List.map Lean.Expr.fvar <$> Mathlib.Deriving.Traversable.getFVarIdsNotImplementationDetails

Instances For

source
def Mathlib.Deriving.Traversable.mkMap (type : Lean.Name) (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

derive the `map` definition of a `Functor`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.deriveFunctor (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

derive the `map` definition and declare `Functor` using this.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.mkInstanceNameForTypeExpr (type : Lean.Expr) :
Lean.Elab.TermElabM Lean.Name

Similar to `mkInstanceName`, but for a `Expr` type.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.mkOneInstance (n cls : Lean.Name) (tac : Lean.MVarId → Lean.Elab.TermElabM Unit) (mkInst : Lean.Name → Lean.Expr → Lean.Elab.TermElabM Lean.Expr := fun (n : Lean.Name) (arg : Lean.Expr) => liftM (Lean.Meta.mkAppM n #[arg])) :
Lean.Elab.TermElabM Unit

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.higherOrderDeriveHandler (cls : Lean.Name) (tac : Lean.MVarId → Lean.Elab.TermElabM Unit) (deps : List Lean.Elab.DerivingHandler := []) (mkInst : Lean.Name → Lean.Expr → Lean.Elab.TermElabM Lean.Expr := fun (n : Lean.Name) (arg : Lean.Expr) => liftM (Lean.Meta.mkAppM n #[arg])) :
Lean.Elab.DerivingHandler

Make the new deriving handler depends on other deriving handlers.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.functorDeriveHandler :
Lean.Elab.DerivingHandler

The deriving handler for `Functor`.

Equations

- Mathlib.Deriving.Traversable.functorDeriveHandler = Mathlib.Deriving.Traversable.higherOrderDeriveHandler `Functor Mathlib.Deriving.Traversable.deriveFunctor

Instances For

source
def Mathlib.Deriving.Traversable.deriveLawfulFunctor (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

Prove the functor laws and derive `LawfulFunctor`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.lawfulFunctorDeriveHandler :
Lean.Elab.DerivingHandler

The deriving handler for `LawfulFunctor`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
partial def Mathlib.Deriving.Traversable.nestedTraverse (f v t : Lean.Expr) :
Lean.Elab.TermElabM Lean.Expr

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

source
def Mathlib.Deriving.Traversable.traverseField (n : Lean.Name) (cl f v e : Lean.Expr) :
Lean.Elab.TermElabM (Bool × Lean.Expr)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.traverseConstructor (c n : Lean.Name) (applInst f α β : Lean.Expr) (args₀ : List Lean.Expr) (args₁ : List (Bool × Lean.Expr)) (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

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.`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor (c : Lean.Name) (args : List (Bool × Lean.Expr)) (fvars aargs : Array Lean.Expr := #[]) :
Lean.Elab.TermElabM Lean.Expr

`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

- One or more equations did not get rendered due to their size.
- Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor c ((false, x) :: xs) fvars aargs = Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor c xs fvars (aargs.push x)
- Mathlib.Deriving.Traversable.traverseConstructor.mkFunCtor c [] fvars aargs = liftM do let e ← Lean.Meta.mkAppOptM c (Array.map some aargs) Lean.Meta.mkLambdaFVars fvars e

Instances For

source
def Mathlib.Deriving.Traversable.mkTraverse (type : Lean.Name) (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

derive the `traverse` definition of a `Traversable` instance

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.deriveTraversable (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

derive the `traverse` definition and declare `Traversable` using this.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.traversableDeriveHandler :
Lean.Elab.DerivingHandler

The deriving handler for `Traversable`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.simpFunctorGoal (m : Lean.MVarId) (s : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray := ∅) (discharge? : Option Lean.Meta.Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array Lean.FVarId := #[]) (stats : Lean.Meta.Simp.Stats := { }) :
Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)

Simplify the goal `m` using `functor_norm`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.traversableLawStarter (m : Lean.MVarId) (n : Lean.Name) (s : Lean.MetaM Lean.Meta.Simp.Context) (tac : Array Lean.FVarId → Lean.Meta.InductionSubgoal → Lean.MVarId → Lean.MetaM Unit) :
Lean.MetaM Unit

Run the following tactic:

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.deriveLawfulTraversable (m : Lean.MVarId) :
Lean.Elab.TermElabM Unit

Prove the traversable laws and derive `LawfulTraversable`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Deriving.Traversable.lawfulTraversableDeriveHandler :
Lean.Elab.DerivingHandler

The deriving handler for `LawfulTraversable`.

Equations

- One or more equations did not get rendered due to their size.

Instances For