Skip to content

Commit d7e4f32

Browse files
authored
feat: Bool.ctorIdx (#11024)
This PR lets `Bool` have `.ctorIdx` like any other inductive.
1 parent c7f57d6 commit d7e4f32

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Init/Prelude.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2216,6 +2216,7 @@ theorem Nat.mod_lt : (x : Nat) → {y : Nat} → (hy : LT.lt 0 y) → LT.lt (HM
22162216
| .isFalse h => Nat.lt_of_not_le h
22172217

22182218
attribute [gen_constructor_elims] Nat
2219+
attribute [gen_constructor_elims] Bool
22192220

22202221
/--
22212222
Gets the word size of the current platform. The word size may be 64 or 32 bits.

0 commit comments

Comments
 (0)