| -- This validates that Lean is able to simplify patterns containing operations | |
| -- on ground natural literals. | |
| -- | |
| -- This is a regression test for #3139. | |
| set_option maxHeartbeats 1000 | |
| -- This fails without the fix and maxHeartbeats 1000. | |
| def testZeroAdd (x:Nat) := | |
| match x with | |
| | 0 + 128 => true | |
| | _ => false | |
| -- This succeeds in all cases | |
| def testAddZero (x:Nat) := | |
| match x with | |
| | 128 + 0 => true | |
| | _ => false | |
| #reduce 128 &&& 128 = 128 | |
| #reduce 128 ||| 128 = 128 | |
| #reduce 128 ^^^ 128 = 0 | |
| #reduce 0 >>> 128 = 0 | |
| #reduce 0 <<< 128 = 0 |