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
Instances For
Get the auxiliary local declaration corresponding to the current declaration. If there are multiple declaraions it will throw.
Instances For
similar to traverseConstructor
but for Functor
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 FVarId
s which is not implementation details in the current context.
Instances For
Get Expr
s of FVarId
s 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
The deriving handler for Functor
.
Instances For
Prove the functor laws and derive LawfulFunctor
.
Instances For
The deriving handler for LawfulFunctor
.
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
- 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 (Array.push aargs x)
Instances For
derive the traverse
definition of a Traversable
instance
Instances For
derive the traverse
definition and declare Traversable
using this.
Instances For
The deriving handler for Traversable
.
Instances For
Simplify the goal m
using functor_norm
.
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
Prove the traversable laws and derive LawfulTraversable
.
Instances For
The deriving handler for LawfulTraversable
.