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

chore: remove unused param

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-29 20:41:30 -07:00
parent e6031925c3
commit dadab54014
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -30,8 +30,7 @@ def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : MetaM (Arra
throwError "argument '{namedArg.name}' was already set"
return namedArgs.push namedArg
set_option linter.unusedVariables.funArgs false in
partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array NamedArg × Array Arg × Bool) := do
partial def expandArgs (args : Array Syntax) : MetaM (Array NamedArg × Array Arg × Bool) := do
let (args, ellipsis) :=
if args.isEmpty then
(args, false)
@ -52,8 +51,7 @@ partial def expandArgs (args : Array Syntax) (pattern := false) : MetaM (Array N
return (namedArgs, args.push $ Arg.stx stx)
return (namedArgs, args, ellipsis)
set_option linter.unusedVariables.funArgs false in
def expandApp (stx : Syntax) (pattern := false) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
def expandApp (stx : Syntax) : MetaM (Syntax × Array NamedArg × Array Arg × Bool) := do
let (namedArgs, args, ellipsis) ← expandArgs stx[1].getArgs
return (stx[0], namedArgs, args, ellipsis)

2
src/Lean/Elab/PatternVar.lean
View file

@ -217,7 +217,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
where
processCtorApp (stx : Syntax) : M Syntax := do
let (f, namedArgs, args, ellipsis) ← expandApp stx true
let (f, namedArgs, args, ellipsis) ← expandApp stx
if f.getKind == ``Parser.Term.dotIdent then
let namedArgsNew ← namedArgs.mapM fun
| { ref, name, val := Arg.stx arg } => withRef ref do `(Lean.Parser.Term.namedArgument| ($(mkIdentFrom ref name) := $(← collect arg)))