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

feat: use at least default transparency at toCtorWhenK

Browse source 
Improves the effectiveness of `simp` when reducing `match`-expr.
This commit is contained in:
Leonardo de Moura 2022-02-12 07:54:48 -08:00
parent 999e80745e
commit 32dd3c6b29
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/WHNF.lean
View file

@ -99,7 +99,10 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
else do
let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure major
let newType ← inferType newCtorApp
if (← isDefEq majorType newType) then
/- TODO: check whether changing reducibility to default hurts performance here.
We do that to make sure auxiliary `Eq.rec` introduced by the `match`-compiler
are reduced even when `TransparencyMode.reducible` (like in `simp`) -/
if (← withAtLeastTransparency TransparencyMode.default <| isDefEq majorType newType) then
return newCtorApp
else
return major