lean4-htt/src/Init/Data/Int
Kim Morrison cb600ed9b4 chore: restore broken proofs
This reverts commit d099f560f72b5f18695c7fb586a9da93af0cb17e.
2024-12-03 17:59:23 +11:00
..
Bitwise chore: restore broken proofs 2024-12-03 17:59:23 +11:00
Basic.lean chore: avoid importing List.Basic without List.Impl (#5245) 2024-09-04 01:25:50 +00:00
Bitwise.lean chore: upstream Std.BitVec.* (#3400) 2024-02-19 12:43:34 -08:00
DivMod.lean chore: rename Int.div/mod to tdiv/tmod (#5301) 2024-09-11 06:15:44 +00:00
DivModLemmas.lean chore: robustify for byAsSorry (#6287) 2024-12-02 23:53:16 +00:00
Gcd.lean chore: upstream Std.Data.Int (#3635) 2024-03-11 21:40:48 +00:00
Lemmas.lean chore: fix naming of left/right injectivity lemmas (#6106) 2024-11-18 00:53:46 +00:00
LemmasAux.lean chore: reverse direction of Int.toNat_sub (#5208) 2024-08-30 02:25:53 +00:00
Order.lean feat: update omega/solve_by_elim to use new tactic syntax, use new tactic syntax (#5932) 2024-11-03 16:23:37 +00:00
Pow.lean chore: restore broken proofs 2024-12-03 17:59:23 +11:00