Skip to content

Commit

Permalink
bump ci
Browse files Browse the repository at this point in the history
  • Loading branch information
hargoniX committed Oct 9, 2024
1 parent 30b0ea9 commit 79eda0d
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/Init/Data/UInt/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,6 @@ declare_uint_theorems UInt32
declare_uint_theorems UInt64
declare_uint_theorems USize


theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]

Expand Down

0 comments on commit 79eda0d

Please sign in to comment.