Skip to content

Commit bd58e35

Browse files
kim-emfgdorais
andauthored
chore: bump toolchain to v4.29.0-rc6 (#1708)
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
1 parent ac3fb72 commit bd58e35

2 files changed

Lines changed: 3 additions & 1 deletion

File tree

Batteries/Data/Bool.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,13 +16,15 @@ WellFoundedGT classes available in Mathlib.
1616
-/
1717

1818
/-- Boolean '<' is well founded -/
19+
@[implicit_reducible]
1920
def Bool.lt_wfRel : WellFoundedRelation Bool where
2021
rel := (· < ·)
2122
wf := ⟨fun
2223
| false => ⟨false, nofun
2324
| true => ⟨true, fun | false, _ => ⟨false, nofun⟩⟩⟩
2425

2526
/-- Boolean '>' is well founded -/
27+
@[implicit_reducible]
2628
def Bool.gt_wfRel : WellFoundedRelation Bool where
2729
rel := (· > ·)
2830
wf := ⟨fun

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.29.0-rc4
1+
leanprover/lean4:v4.29.0-rc6

0 commit comments

Comments
 (0)