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

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.Elab.Deriving.mkImplicitBinders (argNames : Array Lake.Name) :
      Lean.Elab.TermElabM (Array (Lean.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
      • One or more equations did not get rendered due to their size.
      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
        • One or more equations did not get rendered due to their size.
        Instances For
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Lean.Elab.Deriving.mkLet (letDecls : Array (Lean.TSyntax `Lean.Parser.Term.letDecl)) (body : Lean.Term) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Lean.Elab.Deriving.mkDiscr (varName : Lake.Name) :
                    Lean.Elab.TermElabM (Lean.TSyntax `Lean.Parser.Term.matchDiscr)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For