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)

    Instances For

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

      Instances For