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

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

Instances For

    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

                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

                    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

                      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

                        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

                              Run the following tactic:

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