lean4-htt/src/Init/Data
Leonardo de Moura 0893b62598 perf: avoid unnecessary overhead at HashSet
List instead of AssocList saves one word per entry.
2020-03-02 08:40:15 -08:00
..
Array feat: add Array.findIdxM? and Array.getIdx? 2020-02-19 14:54:55 -08:00
BinomialHeap chore: Coe.lean ==> HasCoe.lean 2020-01-28 08:55:22 -08:00
ByteArray chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Char fix: little details 2020-01-12 08:02:48 -08:00
Fin chore: HasModn ==> HasModN 2019-12-11 15:36:58 -08:00
HashMap feat: add findEntry? functions 2020-02-24 15:47:59 -08:00
Int chore: Coe.lean ==> HasCoe.lean 2020-01-28 08:55:22 -08:00
List feat: add List.replace 2020-03-02 08:30:20 -08:00
Nat feat: add new Coe.lean 2020-01-28 13:10:30 -08:00
Option chore: remove coeSortBool 2020-01-28 19:07:02 -08:00
PersistentArray refactor: naming consistency ensure List and Array have similar find* methods 2020-01-26 15:13:05 -08:00
PersistentHashMap chore: variable order consistency 2020-02-24 18:29:24 -08:00
Queue chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
RBMap chore: naming convention 2020-02-09 17:10:20 -08:00
RBTree chore: naming convention 2020-02-09 17:10:20 -08:00
Stack chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
String fix: proper Name literals 2020-01-24 12:38:15 -08:00
Array.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
AssocList.lean feat: add findEntry? functions 2020-02-24 15:47:59 -08:00
Basic.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
BinomialHeap.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
ByteArray.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Char.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
DList.lean feat: add builtin notation 2019-12-11 16:22:23 -08:00
Fin.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Hashable.lean fix: leaks 2019-12-22 15:09:19 -08:00
HashMap.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
HashSet.lean perf: avoid unnecessary overhead at HashSet 2020-03-02 08:40:15 -08:00
Int.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
List.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Nat.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Option.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
PersistentArray.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
PersistentHashMap.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
PersistentHashSet.lean feat: add findEntry? functions 2020-02-24 15:47:59 -08:00
Queue.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Random.lean chore: avoid ^do ... 2019-12-11 06:19:12 -08:00
RBMap.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
RBTree.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Repr.lean feat: change ite and dite argument order 2020-02-03 14:11:29 -08:00
Stack.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
String.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
ToString.lean feat: change ite and dite argument order 2020-02-03 14:11:29 -08:00
UInt.lean feat: file IO using handles 2020-01-12 08:02:48 -08:00