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
        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
            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