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

chore: add support for binop% in patterns

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-30 18:38:44 -07:00
parent ae6703a1d2
commit 0a018f2369
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Match.lean
View file

@ -387,6 +387,10 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
let pat := stx[2]
let pat ← collect pat
`(_root_.namedPattern $id $pat)
else if k == ``Lean.Parser.Term.binop then
let lhs ← collect stx[2]
let rhs ← collect stx[3]
return stx.setArg 2 lhs |>.setArg 3 rhs
else if k == ``Lean.Parser.Term.inaccessible then
return stx
else if k == strLitKind then