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

fix: getMkMatcherInputInContext

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-29 12:44:36 -07:00
parent 95ea0b92ea
commit 941ad84ece
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Match/Match.lean
View file

@ -890,7 +890,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
fvarDecls := localDecls.toList
patterns := patterns.toList : Match.AltLHS }
return { matcherName, matchType, discrInfos := mkArray matcherApp.discrs.size {}, lhss }
return { matcherName, matchType, discrInfos := matcherInfo.discrInfos, lhss }
def withMkMatcherInput