Auxiliary inductive datatype for combining unelaborated syntax and already elaborated expressions. It is used to elaborate applications.
- stx: Lean.Syntax → Lean.Elab.Term.Arg
- expr: Lean.Expr → Lean.Elab.Term.Arg
Instances For
Equations
- Lean.Elab.Term.instInhabitedArg = { default := Lean.Elab.Term.Arg.stx default }
Named arguments created using the notation (x := val)
- ref : Lean.Syntax
- name : Lake.Name
- val : Lean.Elab.Term.Arg
Instances For
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)
:
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)