Documentation

Lean.Elab.Arg

inductive Lean.Elab.Term.Arg:

Type

stx: Lean.Syntax → Lean.Elab.Term.Arg
expr: Lean.Expr → Lean.Elab.Term.Arg

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

instance Lean.Elab.Term.instInhabitedArg:

Inhabited Lean.Elab.Term.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)

instance Lean.Elab.Term.instInhabitedNamedArg:

Inhabited Lean.Elab.Term.NamedArg

Equations

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

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

Lean.MetaM (Array Lean.Elab.Term.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 Lean.Syntax) (pattern : optParam Bool false) :

Lean.MetaM (Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool)

Equations

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

def Lean.Elab.Term.expandApp (stx : Lean.Syntax) (pattern : optParam Bool false) :

Lean.MetaM (Lean.Syntax × Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg × Bool)

Equations

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