We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent c6a2114 commit 69fdb35Copy full SHA for 69fdb35
tests/lean/run/double_match.lean
@@ -0,0 +1,22 @@
1
+/--
2
+trace: [Compiler.saveMono] size: 6
3
+ def foo f x : Option Nat :=
4
+ let _x.1 := f x;
5
+ cases _x.1 : Option Nat
6
+ | Option.none =>
7
+ return _x.1
8
+ | Option.some val.2 =>
9
+ let _x.3 := Nat.add val.2 val.2;
10
+ let _x.4 := some ◾ _x.3;
11
+ return _x.4
12
+-/
13
+#guard_msgs in
14
+set_option trace.Compiler.saveMono true in
15
+def foo (f : Nat → Option Nat) (x : Nat) : Option Nat :=
16
+ if let some val := f x then
17
+ if let some val2 := f x then
18
+ some <| val + val2
19
+ else
20
+ none
21
22
0 commit comments