Documentation

Lean.Elab.Arg

Auxiliary inductive datatype for combining unelaborated syntax and already elaborated expressions. It is used to elaborate applications.

Instances For

Named arguments created using the notation (x := val).

  • name : Lake.Name
  • suppressDeps : Bool

    If true, then make all parameters that depend on this one become implicit. This is used for projection notation, since structure parameters might be explicit for classes.

Instances For
Equations

Add a new named argument to namedArgs, and throw an error if it already contains a named argument with the same name.

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