Lean.Elab.Arg

Lean.Elab.Term.addNamedArg namedArgs namedArg = let _do_jp := fun y => pure (Array.push namedArgs namedArg); if Array.any namedArgs (fun a => namedArg.name == a.name) 0 (Array.size namedArgs) = true then do let y ← Lean.throwError (Lean.toMessageData "argument '" ++ Lean.toMessageData namedArg.name ++ Lean.toMessageData "' was already set") _do_jp y else do let y ← pure PUnit.unit _do_jp y

Equations

Lean.Elab.Term.expandArgs args pattern = let x := if Array.isEmpty args = true then (args, false) else if Lean.Syntax.isOfKind (Array.back args) `Lean.Parser.Term.ellipsis = true then (Array.pop args, true) else (args, false); match x with | (args, ellipsis) => do let discr ← Array.foldlM (fun x stx => match x with | (namedArgs, args) => if (Lean.Syntax.getKind stx == `Lean.Parser.Term.namedArgument) = true then let name := Lean.Name.eraseMacroScopes (Lean.Syntax.getId (Lean.Syntax.getOp stx 1)); let val := Lean.Syntax.getOp stx 3; do let namedArgs ← Lean.Elab.Term.addNamedArg namedArgs { ref := stx, name := name, val := Lean.Elab.Term.Arg.stx val } pure (namedArgs, args) else if (Lean.Syntax.getKind stx == `Lean.Parser.Term.ellipsis) = true then Lean.throwErrorAt stx (Lean.toMessageData "unexpected '..'") else pure (namedArgs, Array.push args (Lean.Elab.Term.Arg.stx stx))) (#[], #[]) args 0 (Array.size args) let x : Array Lean.Elab.Term.NamedArg × Array Lean.Elab.Term.Arg := discr match x with | (namedArgs, args) => pure (namedArgs, args, ellipsis)

Equations