Documentation

Lean.Elab.Deriving.Util

Make fresh, hygienic names for every parameter and index of an inductive declaration.

For example, inductive Foo {α : Type} : Nat → Type will give something like #[`α✝, `a✝].

Equations
    Instances For

      Return the inductive declaration's type applied to the arguments in argNames.

      Equations
        Instances For
          def Lean.Elab.Deriving.mkImplicitBinders (argNames : Array Name) :
          TermElabM (Array (TSyntax `Lean.Parser.Term.implicitBinder))

          Return implicit binder syntaxes for the given argNames. The output matches implicitBinder*.

          For example, #[`foo,`bar] gives `({foo} {bar}).

          Equations
            Instances For

              Return instance binder syntaxes binding className α for every generic parameter α of the inductive indVal for which such a binding is type-correct. argNames is expected to provide names for the parameters (see mkInductArgNames). The output matches instBinder*.

              For example, given inductive Foo {α : Type} (n : Nat) : (β : Type) → Type, where β is an index, invoking mkInstImplicitBinders `BarClass foo #[`α, `n, `β] gives `([BarClass α]).

              Equations
                Instances For
                  Instances For
                    Equations
                      Instances For
                        def Lean.Elab.Deriving.mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) :
                        TermElabM (Array (TSyntax `Lean.Parser.Term.letDecl))
                        Equations
                          Instances For
                            def Lean.Elab.Deriving.mkLet (letDecls : Array (TSyntax `Lean.Parser.Term.letDecl)) (body : Term) :
                            Equations
                              Instances For
                                def Lean.Elab.Deriving.mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor : Bool := true) :
                                Equations
                                  Instances For
                                    def Lean.Elab.Deriving.mkDiscr (varName : Name) :
                                    TermElabM (TSyntax `Lean.Parser.Term.matchDiscr)
                                    Equations
                                      Instances For
                                        Instances For
                                          def Lean.Elab.Deriving.mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) :
                                          Equations
                                            Instances For
                                              def Lean.Elab.Deriving.mkDiscrs (header : Header) (indVal : InductiveVal) :
                                              TermElabM (Array (TSyntax `Lean.Parser.Term.matchDiscr))
                                              Equations
                                                Instances For