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.

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

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

similar to traverseField but for Functor

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.

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

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.

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

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

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

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

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

derive the map definition of a Functor

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

derive the map definition and declare Functor using this.

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

Similar to mkInstanceName, but for a Expr type.

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.

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.

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

The deriving handler for Functor.

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

Prove the functor laws and derive LawfulFunctor.

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

The deriving handler for LawfulFunctor.

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

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.

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.

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

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

derive the traverse definition of a Traversable instance

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

derive the traverse definition and declare Traversable using this.

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

The deriving handler for Traversable.

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.

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:

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

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

Prove the traversable laws and derive LawfulTraversable.

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

The deriving handler for LawfulTraversable.