chore: add stage0 stdlib_flags.h update reminder

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/Match/Match.lean

@@ -1094,6 +1094,9 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) (isSplitte
       -- matcher bodies should always be exported, if not private anyway
       withExporting do
         addDecl decl
+      -- if `matcher` is not private, we mark it as `implicit_reducible` too
+      unless isPrivateName name do
+        setReducibilityStatus name .implicitReducible
       unless isSplitter do
         modifyEnv fun env => matcherExt.modifyState env fun s => s.insert key name
         addMatcherInfo name mi

stage0/src/stdlib_flags.h

@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"
 
 namespace lean {

tests/elab/1179b.lean.out.expected

@@ -1,4 +1,4 @@
-def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
+@[implicit_reducible] def Foo.bar.match_1.{u_1} : {l₂ : Nat} →
   (motive : Foo l₂ → Sort u_1) →
     (t₂ : Foo l₂) → ((s₁ : Foo l₂) → motive s₁.cons) → ((x : Foo l₂) → motive x) → motive t₂ :=
 fun {l₂} motive t₂ h_1 h_2 =>

tests/elab/depElim1.lean.out.expected

@@ -1,8 +1,8 @@
 elimTest0 : forall (motive : Nat -> Sort.{u_1}) (x : Nat), (forall (y : Nat), motive y) -> (motive x)
-def elimTest0.{u_1} : (motive : Nat → Sort u_1) → (x : Nat) → ((y : Nat) → motive y) → motive x :=
+@[implicit_reducible] def elimTest0.{u_1} : (motive : Nat → Sort u_1) → (x : Nat) → ((y : Nat) → motive y) → motive x :=
 fun motive x h_1 => h_1 x
 elimTest1 : forall (α : Type.{u_1}) (β : Type.{u_2}) (motive : (List.{u_1} α) -> (List.{u_2} β) -> Sort.{u_3}) (x : List.{u_1} α) (y : List.{u_2} β), (Unit -> (motive (List.nil.{u_1} α) (List.nil.{u_2} β))) -> (forall (a : α) (as : List.{u_1} α) (b : β) (bs : List.{u_2} β), motive (List.cons.{u_1} α a as) (List.cons.{u_2} β b bs)) -> (forall (a : α) (as : List.{u_1} α), motive (List.cons.{u_1} α a as) (List.nil.{u_2} β)) -> (forall (b : β) (bs : List.{u_2} β), motive (List.nil.{u_1} α) (List.cons.{u_2} β b bs)) -> (motive x y)
-def elimTest1.{u_1, u_2, u_3} : (α : Type u_1) →
+@[implicit_reducible] def elimTest1.{u_1, u_2, u_3} : (α : Type u_1) →
   (β : Type u_2) →
     (motive : List α → List β → Sort u_3) →
       (x : List α) →
@@ -15,7 +15,7 @@ fun α β motive x y h_1 h_2 h_3 h_4 =>
   List.casesOn x (List.casesOn y (h_1 ()) fun head tail => h_4 head tail) fun head tail =>
     List.casesOn y (h_3 head tail) fun head_1 tail_1 => h_2 head tail head_1 tail_1
 elimTest2 : forall (α : Type.{u_1}) (motive : forall (n : Nat), (Vec.{u_1} α n) -> (Vec.{u_1} α n) -> Sort.{u_2}) (n : Nat) (xs : Vec.{u_1} α n) (ys : Vec.{u_1} α n), (Unit -> (motive ([mdata _inaccessible:1 OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)]) (Vec.nil.{u_1} α) (Vec.nil.{u_1} α))) -> (forall (n : Nat) (x : α) (xs : Vec.{u_1} α n) (y : α) (ys : Vec.{u_1} α n), motive ([mdata _inaccessible:1 HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) n (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))]) (Vec.cons.{u_1} α n x xs) (Vec.cons.{u_1} α n y ys)) -> (motive n xs ys)
-def elimTest2.{u_1, u_2} : (α : Type u_1) →
+@[implicit_reducible] def elimTest2.{u_1, u_2} : (α : Type u_1) →
   (motive : (n : Nat) → Vec α n → Vec α n → Sort u_2) →
     (n : Nat) →
       (xs ys : Vec α n) →
@@ -47,7 +47,7 @@ fun α motive n xs ys h_1 h_2 =>
         ⋯ xs ys)
     ⋯ ⋯
 elimTest3 : forall (α : Type.{u_1}) (β : Type.{u_2}) (motive : (List.{u_1} α) -> (List.{u_2} β) -> Sort.{u_3}) (x : List.{u_1} α) (y : List.{u_2} β), (Unit -> (motive (List.nil.{u_1} α) (List.nil.{u_2} β))) -> (forall (a : α) (b : β), motive (List.cons.{u_1} α a (List.nil.{u_1} α)) (List.cons.{u_2} β b (List.nil.{u_2} β))) -> (forall (a₁ : α) (a₂ : α) (as : List.{u_1} α) (b₁ : β) (b₂ : β) (bs : List.{u_2} β), motive (List.cons.{u_1} α a₁ (List.cons.{u_1} α a₂ as)) (List.cons.{u_2} β b₁ (List.cons.{u_2} β b₂ bs))) -> (forall (as : List.{u_1} α) (bs : List.{u_2} β), motive as bs) -> (motive x y)
-def elimTest3.{u_1, u_2, u_3} : (α : Type u_1) →
+@[implicit_reducible] def elimTest3.{u_1, u_2, u_3} : (α : Type u_1) →
   (β : Type u_2) →
     (motive : List α → List β → Sort u_3) →
       (x : List α) →

tests/elab/issue10749.lean

@@ -10,7 +10,7 @@ def test (a : List Nat) : Nat :=
 -- Should have no `casesOn`
 
 /--
-info: def test.match_1.{u_1} : (motive : List Nat → Sort u_1) →
+info: @[implicit_reducible] def test.match_1.{u_1} : (motive : List Nat → Sort u_1) →
   (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
 fun motive a h_1 h_2 => h_1 a
 -/
@@ -25,7 +25,7 @@ def test2 (a b : List Nat) : Nat :=
 -- Should have exactly two `casesOn`
 
 /--
-info: def test2.match_1.{u_1} : (motive : List Nat → List Nat → Sort u_1) →
+info: @[implicit_reducible] def test2.match_1.{u_1} : (motive : List Nat → List Nat → Sort u_1) →
   (a b : List Nat) →
     ((x : List Nat) → motive [] x) →
       ((x : List Nat) → motive x []) →
@@ -47,7 +47,7 @@ def test3 (a : List Nat) (b : Bool) : Nat :=
 -- Should have exactly two `casesOn`
 
 /--
-info: def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
+info: @[implicit_reducible] def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
   (a : List Nat) →
     (b : Bool) →
       ((x : List Nat) → motive x true) →
@@ -71,7 +71,7 @@ def test4 : Bool → Bool → Bool → Bool → Bool → Bool
   | _ , _ , _ , _ , _ => false
 
 /--
-info: def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
+info: @[implicit_reducible] def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
   (x x_1 x_2 x_3 x_4 : Bool) →
     ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 x_7 true) →
       ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 true x_7) →
@@ -98,7 +98,7 @@ def test4' : Bool → Bool → Bool → Bool → Bool → Bool
   | false, false, false, false, false => false
 
 /--
-info: def test4'.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
+info: @[implicit_reducible] def test4'.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bool → Sort u_1) →
   (x x_1 x_2 x_3 x_4 : Bool) →
     ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 x_7 true) →
       ((x x_5 x_6 x_7 : Bool) → motive x x_5 x_6 true x_7) →
@@ -130,7 +130,7 @@ def testOld (a : List Nat) : Nat :=
 -- Has unnecessary `casesOn`
 
 /--
-info: def testOld.match_1.{u_1} : (motive : List Nat → Sort u_1) →
+info: @[implicit_reducible] def testOld.match_1.{u_1} : (motive : List Nat → Sort u_1) →
   (a : List Nat) → ((x : List Nat) → motive x) → (Unit → motive []) → motive a :=
 fun motive a h_1 h_2 => test3._sparseCasesOn_2 a (h_1 []) fun h => h_1 a
 -/

tests/elab/issue11211.lean

@@ -13,7 +13,7 @@ def f (xs : List Nat) : Nat :=
   | _ => 2
 
 /--
-info: def f.match_1.{u_1} : (motive : List Nat → Sort u_1) →
+info: @[implicit_reducible] def f.match_1.{u_1} : (motive : List Nat → Sort u_1) →
   (xs : List Nat) → (Unit → motive []) → ((x : List Nat) → motive x) → motive xs
 -/
 #guard_msgs in
@@ -62,7 +62,7 @@ def Option_map (f : α → β) : Option α → Option β
   | none   => none
 
 /--
-info: def Option_map.match_1.{u_1, u_2} : {α : Type u_1} →
+info: @[implicit_reducible] def Option_map.match_1.{u_1, u_2} : {α : Type u_1} →
   (motive : Option α → Sort u_2) → (x : Option α) → ((x : α) → motive (some x)) → (Unit → motive none) → motive x
 -/
 #guard_msgs in

tests/elab/matchSparse.lean

@@ -10,7 +10,7 @@ def simple : Lean.Expr → Bool
   | _      => false
 
 /--
-info: def simple.match_1.{u_1} : (motive : Expr → Sort u_1) →
+info: @[implicit_reducible] def simple.match_1.{u_1} : (motive : Expr → Sort u_1) →
   (x : Expr) → ((u : Level) → motive (sort u)) → ((x : Expr) → motive x) → motive x :=
 fun motive x h_1 h_2 => simple._sparseCasesOn_1 x (fun u => h_1 u) fun h => h_2 x
 -/

tests/elab/match_expose_implicit_reducible.lean

@@ -0,0 +1,49 @@
+module
+
+public def foo : Nat → Nat
+  | 0 => 1
+  | 1 => 3
+  | 2 => 5
+  | x+3 => foo x
+
+@[expose, implicit_reducible] public def bla : Nat → Nat
+  | 0 => 1
+  | 1 => 3
+  | 2 => 5
+  | x+3 => bla x
+
+public abbrev boo : Nat → Nat
+  | 0 => 1
+  | 1 => 3
+  | 2 => 5
+  | _ => 7
+
+/--
+info: private def foo.match_1.{u_1} : (motive : Nat → Sort u_1) →
+  (x : Nat) →
+    (Unit → motive 0) → (Unit → motive 1) → (Unit → motive 2) → ((x : Nat) → motive x.succ.succ.succ) → motive x :=
+fun motive x h_1 h_2 h_3 h_4 =>
+  Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => Nat.casesOn n (h_3 ()) fun n => h_4 n
+-/
+#guard_msgs in
+#print foo.match_1
+
+/--
+info: @[implicit_reducible, expose] def bla.match_1.{u_1} : (motive : Nat → Sort u_1) →
+  (x : Nat) →
+    (Unit → motive 0) → (Unit → motive 1) → (Unit → motive 2) → ((x : Nat) → motive x.succ.succ.succ) → motive x :=
+fun motive x h_1 h_2 h_3 h_4 =>
+  Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => Nat.casesOn n (h_3 ()) fun n => h_4 n
+-/
+#guard_msgs in
+#print bla.match_1
+
+/--
+info: @[implicit_reducible, expose] def boo.match_1.{u_1} : (motive : Nat → Sort u_1) →
+  (x : Nat) → (Unit → motive 0) → (Unit → motive 1) → (Unit → motive 2) → ((x : Nat) → motive x) → motive x :=
+fun motive x h_1 h_2 h_3 h_4 =>
+  dite (x = 0) (Eq.ndrec_symm (h_1 ())) fun h_1 =>
+    dite (x = 1) (Eq.ndrec_symm (h_2 ())) fun h_2 => dite (x = 2) (Eq.ndrec_symm (h_3 ())) fun h_3 => h_4 x
+-/
+#guard_msgs in
+#print boo.match_1

tests/elab/match_nat.lean

@@ -6,7 +6,7 @@ def f : Nat → Nat
 
 
 /--
-info: def f.match_1.{u_1} : (motive : Nat → Sort u_1) →
+info: @[implicit_reducible] def f.match_1.{u_1} : (motive : Nat → Sort u_1) →
   (x : Nat) → (Unit → motive 0) → (Unit → motive 10) → (Unit → motive 100) → ((x : Nat) → motive x) → motive x
 -/
 #guard_msgs in