inductive Lean.Elab.Term.Arg : Type

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

• stx (val : Syntax) : Arg
• expr (val : Expr) : Arg

@[implicit_reducible]

instance Lean.Elab.Term.instInhabitedArg : Inhabited Arg

@[implicit_reducible]

instance Lean.Elab.Term.instToStringArg : ToString Arg

@[implicit_reducible]

instance Lean.Elab.Term.instToMessageDataArg : ToMessageData Arg

structure Lean.Elab.Term.NamedArg : Type

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

• ref : Syntax
• name : Name
• val : Arg
• numImplicitParams : Nat

  Overrides the binder infos for the first numImplicitParams parameters to make them be implicit if they were explicit. This is used for expanding projection notation. The primary motivation for this field is that class projections may feature explicit structure parameters. See the note at Lean.Elab.Term.ElabAppArgs.processExplicitArg.

@[implicit_reducible]

instance Lean.Elab.Term.instInhabitedNamedArg : Inhabited NamedArg

@[implicit_reducible]

instance Lean.Elab.Term.instToStringNamedArg : ToString NamedArg

@[implicit_reducible]

instance Lean.Elab.Term.instToMessageDataNamedArg : ToMessageData NamedArg

def Lean.Elab.Term.addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : MetaM (Array NamedArg)

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

def Lean.Elab.Term.expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Arg × Bool)

def Lean.Elab.Term.expandApp (stx : Syntax) : MetaM (Syntax × Array NamedArg × Array Arg × Bool)