Skip to content

Commit

Permalink
chore: add a few tests
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Nov 29, 2024
1 parent 6d8b413 commit e462b97
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions tests/lean/simprocUInt.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
variable (x : USize)

/- USize.toNat -/

#check_simp USize.toNat 4294967296 !~>
#check_simp USize.toNat 4294967295 ~> 4294967295
#check_simp USize.toNat (x &&& 1) ~> x.toNat % 2

0 comments on commit e462b97

Please sign in to comment.