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

fix: out-of-bounds array access

Browse source
This commit is contained in:
Gabriel Ebner 2021-10-15 19:40:09 +02:00 • committed by Sebastian Ullrich
parent b3c8ee2923
commit d379cd6853
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Syntax.lean
View file

@ -342,8 +342,7 @@ def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
given == expected || given == expected ++ `antiquot
def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
| `(matchAltExpr| | $pats,* => $rhs) => do
let pat := pats.elemsAndSeps[0]
| `(matchAltExpr| | $pat:term => $rhs) => do
if !pat.isQuot then
throwUnsupportedSyntax
let quoted := getQuotContent pat