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

instance Lean.Elab.Term.instInhabitedArg : Inhabited Arg

Equations

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

structure Lean.Elab.Term.NamedArg : Type

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

• ref : Syntax
• name : Name
• val : Arg
• 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.

instance Lean.Elab.Term.instInhabitedNamedArg : Inhabited NamedArg

Equations

• Lean.Elab.Term.instInhabitedNamedArg = { default := { ref := default, name := default, val := default, suppressDeps := default } }

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 __discr ← Lean.Elab.Term.expandArgs stx[1].getArgs match __discr with | (namedArgs, args, ellipsis) => pure (stx[0], namedArgs, args, ellipsis)