Eric Wieser 8cd9ce0684 refactor: redefine Nat.mod such that rfl : 0 % n = 0 ... This property was true in Lean 3, and it was very convenient for working with `Fin n`.		2023-01-11 09:49:58 -08:00
..
Basic.lean	chore: rename le_or_eq_or_le_succ (#2024)	2023-01-09 09:45:51 -08:00
Bitwise.lean	feat: show bitwise terminates	2022-06-12 14:01:05 -07:00
Control.lean	chore: fix codebase and tests	2021-06-29 17:14:52 -07:00
Div.lean	refactor: redefine Nat.mod such that rfl : 0 % n = 0	2023-01-11 09:49:58 -08:00
Gcd.lean	refactor: redefine Nat.mod such that rfl : 0 % n = 0	2023-01-11 09:49:58 -08:00
Linear.lean	chore: fix build	2022-11-28 07:53:43 -08:00
Log2.lean	feat: log2 for Fin and UInts	2022-11-29 01:05:06 +01:00
Power2.lean	feat: add Power2	2022-10-27 18:11:20 -07:00
SOM.lean	chore: remove staging workarounds	2022-04-26 08:23:43 -07:00