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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    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

      similar to traverseConstructor but for Functor

      Equations
      • One or more equations did not get rendered due to their size.
      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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            derive the map definition of a Functor

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              derive the map definition and declare Functor using this.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Similar to mkInstanceName, but for a Expr type.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  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

                    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

                      Prove the functor laws and derive LawfulFunctor.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The deriving handler for LawfulFunctor.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          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.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  derive the traverse definition and declare Traversable using this.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The deriving handler for Traversable.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Mathlib.Deriving.Traversable.simpFunctorGoal (m : Lean.MVarId) (s : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray ) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { map := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } } }) :

                                      Simplify the goal m using functor_norm.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Run the following tactic:

                                        intros _ .. 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

                                          Prove the traversable laws and derive LawfulTraversable.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            The deriving handler for LawfulTraversable.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For