Avoid simpleBinder nesting
#1296
Conversation
|
The code changes suggest that it would be nice to have |
Yes, that's a very good idea. Please also unify it with |
| | ``Lean.Parser.Term.strictImplicitBinder | ||
| | ``Lean.Parser.Term.instBinder | ||
| | ``Lean.Parser.Term.explicitBinder | ||
| | ``Lean.Parser.Term.hole | `ident => loop body (i+1) (newBinders.push binder) |
There was a problem hiding this comment.
Nice. It is great to see new features making our code cleaner :)
| @@ -552,7 +558,7 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax := | |||
|
|
|||
| open Lean.Elab.Term.Quotation in | |||
| @[builtinQuotPrecheck Lean.Parser.Term.fun] def precheckFun : Precheck | |||
| | `(fun $binders* => $body) => do | |||
| | `(fun $binders* $[: $ty?]? => $body) => do | |||
There was a problem hiding this comment.
Should we use _ty to avoid the warning from the unused variable linter?
There was a problem hiding this comment.
Ah, not sure why I didn't see the warning. Will fix when I'm home.
| views[0]!.binders.getArgs.all (·.getKind == ``Parser.Term.simpleBinder) then | ||
| some <| (views[0]!.binders.getArgs.toList.map (fun stx => stx[0].getArgs.toList.map (·.getId))).join | ||
| views[0]!.binders.getArgs.all (·.isIdent) then | ||
| some (views[0]!.binders.getArgs.toList.map (·.getId)) |
I think this is a good idea, but we can use another PR for this unification. |
|
@Kha The failure has nothing to do with this PR. Please feel free to merge it as-is. |
See #1272 (comment)