Skip to content

Commit fda0b93

Browse files
committed
chore: remove comments about missing functionality now implemented elsewhere
1 parent a7af9f7 commit fda0b93

File tree

2 files changed

+0
-6
lines changed

2 files changed

+0
-6
lines changed

src/Lean/Compiler/LCNF/ToDecl.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -131,11 +131,6 @@ def toDecl (declName : Name) : CompilerM Decl := do
131131
let value ← inlineMatchers value
132132
/- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/
133133
let value ← macroInline value
134-
/-
135-
Remark: we have disabled the following transformatbion, we will perform it at phase 2, after code specialization.
136-
It prevents many optimizations (e.g., "cases-of-ctor").
137-
-/
138-
-- let value ← applyCasesOnImplementedBy value
139134
return (type, value)
140135
let code ← toLCNF value
141136
let decl ← if let .fun decl (.return _) := code then

src/Lean/Compiler/LCNF/ToMono.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,6 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do
278278
else if let some info ← hasTrivialStructure? c.typeName then
279279
trivialStructToMono info c
280280
else
281-
-- TODO: `casesOn` `[implemented_by]` support
282281
let type ← toMonoType c.resultType
283282
let alts ← c.alts.mapM fun alt =>
284283
match alt with

0 commit comments

Comments
 (0)