max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/data
History
Leonardo de Moura 67a4ebbde6 feat(library/init/lean/attributes): low level attribute registration, and frontend attribute actions 
Remark: the attribute actions used by the frontend are all in IO.
These actions access attributes by name, and need access to the IO.ref
that contains all registered attributes in the system.
2019-06-05 09:15:35 -07:00
..
array feat(library/init/data/array/basic): efficient heterogeneous Array.map 2019-05-25 16:32:59 -07:00
bytearray refactor(library/init/lean/environment): cleanup and improve 2019-05-10 15:54:29 -07:00
char refactor(library/init/data/rbmap): use Bool instead of Prop 2019-04-03 02:54:34 -07:00
fin chore(library/init/core): HasLt => HasLess, HasLe => HasLessEq, ... 2019-03-23 10:07:46 -07:00
hashmap feat(library/init/lean/attributes): low level attribute registration, and frontend attribute actions 2019-06-05 09:15:35 -07:00
int refactor(library): remove now-redundant parentheses 2019-05-03 13:57:21 +02:00
list feat(library/init/data): add ByteArray 2019-05-08 16:43:00 -07:00
nat feat(library/init/data/nat/bitwise): use lean::nat_land and lean::nat_lor 2019-05-31 21:55:57 -07:00
option feat(library/init/data/option/basic): add [inline] attributes 2019-03-28 20:18:37 -07:00
ordering refactor(library): remove now-redundant parentheses 2019-05-03 13:57:21 +02:00
persistentarray feat(library/init/data/persistentarray/basic): add PersistentArray.modify 2019-06-04 10:40:46 -07:00
rbmap feat(library/init/lean/environment): show rbmap depth and hashmap bucket size 2019-05-15 11:01:25 -07:00
rbtree feat(library/init/data/rbmap): add erase 2019-05-04 15:58:30 -07:00
string chore(library): toBool ==> decide 2019-05-06 14:02:15 -07:00
assoclist.lean feat(library/init/lean/attributes): low level attribute registration, and frontend attribute actions 2019-06-05 09:15:35 -07:00
basic.lean chore(library): use lowercase in imports 2019-03-21 15:06:44 -07:00
default.lean feat(library/init/data): add ByteArray 2019-05-08 16:43:00 -07:00
dlist.lean refactor(library/init): move function.lean definitions to core.lean 2019-03-22 09:33:10 -07:00
hashable.lean feat(runtime): add primitive hash functions 2019-04-03 04:01:36 -07:00
random.lean feat(library/init/data/random): random numbers 2019-05-04 15:57:42 -07:00
repr.lean feat(library/init/data/string): add Substring 2019-03-25 09:29:06 -07:00
tostring.lean feat(library/init/data/string): add Substring 2019-03-25 09:29:06 -07:00
uint.lean feat(library/init/data/uint): add shift_left and shift_right 2019-06-01 10:57:08 -07:00