diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean index 500a9fd10b..7e4f1bcb39 100644 --- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean +++ b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean @@ -61,8 +61,7 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do | some { value := .const declName _ args, .. } => let some (.ctorInfo val) := (← getEnv).find? declName | return none return some <| .ctor val args - | some _ => return none - | none => return (← read).discrCtorMap.get? fvarId + | _ => return (← read).discrCtorMap.get? fvarId def findCtorName? (fvarId : FVarId) : DiscrM (Option Name) := do let some ctorInfo ← findCtor? fvarId | return none diff --git a/tests/lean/run/double_match.lean b/tests/lean/run/double_match.lean new file mode 100644 index 0000000000..b944c7cdb8 --- /dev/null +++ b/tests/lean/run/double_match.lean @@ -0,0 +1,22 @@ +/-- +trace: [Compiler.saveMono] size: 6 + def foo f x : Option Nat := + let _x.1 := f x; + cases _x.1 : Option Nat + | Option.none => + return _x.1 + | Option.some val.2 => + let _x.3 := Nat.add val.2 val.2; + let _x.4 := some ◾ _x.3; + return _x.4 +-/ +#guard_msgs in +set_option trace.Compiler.saveMono true in +def foo (f : Nat → Option Nat) (x : Nat) : Option Nat := + if let some val := f x then + if let some val2 := f x then + some <| val + val2 + else + none + else + none