Skip to content

Commit c6a2114

Browse files
committed
perf: better detection of repeated branching on same value
1 parent e11ef3e commit c6a2114

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/Lean/Compiler/LCNF/Simp/DiscrM.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,8 +61,7 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do
6161
| some { value := .const declName _ args, .. } =>
6262
let some (.ctorInfo val) := (← getEnv).find? declName | return none
6363
return some <| .ctor val args
64-
| some _ => return none
65-
| none => return (← read).discrCtorMap.get? fvarId
64+
| _ => return (← read).discrCtorMap.get? fvarId
6665

6766
def findCtorName? (fvarId : FVarId) : DiscrM (Option Name) := do
6867
let some ctorInfo ← findCtor? fvarId | return none

0 commit comments

Comments
 (0)