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

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-13 19:35:47 -07:00
parent fc6f9324ac
commit d52de3392b
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/IndPredBelow.lean
View file

@ -428,7 +428,7 @@ partial def mkBelowMatcher
| _, _ => xs
let t := t.replaceFVars xs[:oldFVars.size] fvars[:oldFVars.size]
trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]}"
let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]).toArray t
let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]) t
trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
newAlt