Documentation

Lean.Elab.Deriving.Basic

Result for mkInst?

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

      A DerivingHandler is called on the fully qualified names of all types it is running for as well as the syntax of a with argument, if present.

      For example, deriving instance Foo with fooArgs for Bar, Baz invokes fooHandler #[`Bar, `Baz] `(fooArgs).

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

        Like registerBuiltinDerivingHandlerWithArgs but ignoring any with argument.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.Elab.applyDerivingHandlers (className : Lake.Name) (typeNames : Array Lake.Name) (args? : Option (Lean.TSyntax `Lean.Parser.Term.structInst)) :
            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
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For