Skip to content

Commit f4c71f6

Browse files
authored
fix: simplify Nat.ble (#11058)
This PR changes `Nat.ble` by joining the two `Nat.ble Nat.zero _` cases into one, allowing `decide (0 <= x) = true` and `decide (0 < succ x) = true` to be solvable by `rfl`.
1 parent 823173a commit f4c71f6

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/Init/Prelude.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1831,8 +1831,7 @@ Examples:
18311831
-/
18321832
@[extern "lean_nat_dec_le"]
18331833
def Nat.ble : @& Nat → @& Nat → Bool
1834-
| zero, zero => true
1835-
| zero, succ _ => true
1834+
| zero, _ => true
18361835
| succ _, zero => false
18371836
| succ n, succ m => ble n m
18381837

0 commit comments

Comments
 (0)