max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: move methods to MetaM

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-10 10:00:46 -08:00
parent 2fb9a39cb4
commit 7a39be225d
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Arg.lean
View file

@ -25,12 +25,12 @@ structure NamedArg where
/--
Add a new named argument to `namedArgs`, and throw an error if it already contains a named argument
with the same name. -/
def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : TermElabM (Array NamedArg) := do
def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : MetaM (Array NamedArg) := do
if namedArgs.any (namedArg.name == ·.name) then
throwError "argument '{namedArg.name}' was already set"
return namedArgs.push namedArg
partial def expandArgs (args : Array Syntax) (pattern := false) : TermElabM (Array NamedArg × Array Arg × Bool) := do
partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array NamedArg × Array Arg × Bool) := do
let (args, ellipsis) :=
if args.isEmpty then
(args, false)
@ -51,7 +51,7 @@ partial def expandArgs (args : Array Syntax) (pattern := false) : TermElabM (Arr
return (namedArgs, args.push $ Arg.stx stx)
return (namedArgs, args, ellipsis)
def expandApp (stx : Syntax) (pattern := false) : TermElabM (Syntax × Array NamedArg × Array Arg × Bool) := do
def expandApp (stx : Syntax) (pattern := false) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
let (namedArgs, args, ellipsis) ← expandArgs stx[1].getArgs
return (stx[0], namedArgs, args, ellipsis)