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

chore: remove leftover

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-09 11:55:30 -07:00
parent 613c8027d7
commit e81673366a
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Compiler/LCNF/ToLCNF.lean
View file

@ -504,7 +504,6 @@ where
ps ← ps.mapM fun p => do
let type ← inferType p.toExpr
if (← isTypeFormerType type) then
trace[Meta.debug] "{p.binderName} is type former"
modify fun s => { s with toAny := s.toAny.insert p.fvarId }
/-
Recall that we may have dependent fields. Example: