Create ctorIdx for Bool

Author: nomeata

src/Init/Prelude.lean

@@ -2216,6 +2216,7 @@ theorem Nat.mod_lt : (x : Nat) →  {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HM
       | .isFalse h => Nat.lt_of_not_le h
 
 attribute [gen_constructor_elims] Nat
+attribute [gen_constructor_elims] Bool
 
 /--
 Gets the word size of the current platform. The word size may be 64 or 32 bits.

tests/lean/run/issue10749.lean

@@ -52,7 +52,8 @@ info: def test3.match_1.{u_1} : (motive : List Nat → Bool → Sort u_1) →
     (b : Bool) →
       ((x : List Nat) → motive x true) →
         ((x : Bool) → motive [] x) → ((x : List Nat) → (x_1 : Bool) → motive x x_1) → motive a b :=
-fun motive a b h_1 h_2 h_3 => Bool.casesOn b (test3._sparseCasesOn_1 a (h_2 false) fun h_0 => h_3 a false) (h_1 a)
+fun motive a b h_1 h_2 h_3 =>
+  test3._sparseCasesOn_1 b (h_1 a) fun h_0 => test3._sparseCasesOn_2 a (h_2 b) fun h_0 => h_3 a b
 -/
 #guard_msgs in #print test3.match_1
 
@@ -79,14 +80,11 @@ info: def test4.match_1.{u_1} : (motive : Bool → Bool → Bool → Bool → Bo
             ((x x_5 x_6 x_7 : Bool) → motive true x x_5 x_6 x_7) →
               ((x x_5 x_6 x_7 x_8 : Bool) → motive x x_5 x_6 x_7 x_8) → motive x x_1 x_2 x_3 x_4 :=
 fun motive x x_1 x_2 x_3 x_4 h_1 h_2 h_3 h_4 h_5 h_6 =>
-  Bool.casesOn x_4
-    (Bool.casesOn x_3
-      (Bool.casesOn x_2
-        (Bool.casesOn x_1 (Bool.casesOn x (h_6 false false false false false) (h_5 false false false false))
-          (h_4 x false false false))
-        (h_3 x x_1 false false))
-      (h_2 x x_1 x_2 false))
-    (h_1 x x_1 x_2 x_3)
+  test3._sparseCasesOn_1 x_4 (h_1 x x_1 x_2 x_3) fun h_0 =>
+    test3._sparseCasesOn_1 x_3 (h_2 x x_1 x_2 x_4) fun h_0 =>
+      test3._sparseCasesOn_1 x_2 (h_3 x x_1 x_3 x_4) fun h_0 =>
+        test3._sparseCasesOn_1 x_1 (h_4 x x_2 x_3 x_4) fun h_0 =>
+          test3._sparseCasesOn_1 x (h_5 x_1 x_2 x_3 x_4) fun h_0 => h_6 x x_1 x_2 x_3 x_4
 -/
 #guard_msgs in
 #print test4.match_1
@@ -134,7 +132,7 @@ def testOld (a : List Nat) : Nat :=
 /--
 info: 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_1 a (h_1 []) fun h_0 => h_1 a
+fun motive a h_1 h_2 => test3._sparseCasesOn_2 a (h_1 []) fun h_0 => h_1 a
 -/
 #guard_msgs in
 #print testOld.match_1