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

Equations

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

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.

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.

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.

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

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

Equations

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

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

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

Equations

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

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.

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.

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.

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.

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.

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

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.

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.

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.

Equations

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

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.

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

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.

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.

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.

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 := { 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 } } }) : 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.

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)

Equations

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

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.

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.