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

Equations

• Lean.Elab.Term.instInhabitedArg = { default := Lean.Elab.Term.instInhabitedArg.default }

@[implicit_reducible]

instance Lean.Elab.Term.instToStringArg : ToString Arg

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.Term.instToMessageDataArg : ToMessageData Arg

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Term.instInhabitedNamedArg = { default := Lean.Elab.Term.instInhabitedNamedArg.default }

@[implicit_reducible]

instance Lean.Elab.Term.instToStringNamedArg : ToString NamedArg

Equations

• Lean.Elab.Term.instToStringNamedArg = { toString := fun (s : Lean.Elab.Term.NamedArg) => toString "(" ++ toString s.name ++ toString " := " ++ toString s.val ++ toString ")" }

@[implicit_reducible]

instance Lean.Elab.Term.instToMessageDataNamedArg : ToMessageData NamedArg

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Term.expandApp stx = do let __x ← Lean.Elab.Term.expandArgs stx[1].getArgs match __x with | (namedArgs, args, ellipsis) => pure (stx[0], namedArgs, args, ellipsis)