Skip to content

Commit d2bd7a4

Browse files
committed
simplify Nat.ble
1 parent 51ef1dc commit d2bd7a4

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)