Skip to content

Commit 91b99d4

Browse files
remove dead code: updateViewRemovingFunctorName
This is based on feedback from the PR.
1 parent 18d7eba commit 91b99d4

File tree

1 file changed

+0
-4
lines changed

1 file changed

+0
-4
lines changed

src/Lean/Elab/MutualInductive.lean

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1146,10 +1146,6 @@ def updateViewWithFunctorName (view : InductiveView) : InductiveView :=
11461146
let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (addFunctorPostfix ctor.declName.getPrefix)})
11471147
{view with declName := addFunctorPostfix view.declName, ctors := newCtors}
11481148

1149-
def updateViewRemovingFunctorName (view : InductiveView) : InductiveView :=
1150-
let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (removeFunctorPostfix ctor.declName.getPrefix)})
1151-
{view with declName := addFunctorPostfix view.declName, ctors := newCtors}
1152-
11531149
private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
11541150
let view0 := elabs[0]!.view
11551151
let ref := view0.ref

0 commit comments

Comments
 (0)