Documentation

Lean.Elab.Deriving.Basic

Result for mkInst?

Equations
  • One or more equations did not get rendered due to their size.
@[deprecated Lean.Elab.DerivingHandler]

Deprecated - DerivingHandler no longer assumes arguments

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