mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
1118931516
This adds bitwise operations to reduceNat? and the kernel. It incorporates some basic test cases to validate the correct operations are associated.
24 lines
544 B
Lean4
24 lines
544 B
Lean4
-- 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
|