lean4-htt/library/init/data
Sebastian Ullrich 3ed67138d5 chore(*): update equation syntax in files and old parser
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
2019-08-09 11:11:34 +02:00
..
array chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
binomialheap chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
bytearray chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
char chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
fin chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
hashmap chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
int chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
list chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
nat chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
option chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
ordering chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
persistentarray chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
persistenthashmap chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
rbmap chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
rbtree chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
string chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
assoclist.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02: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 chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
hashable.lean feat(runtime): add primitive hash functions 2019-04-03 04:01:36 -07:00
random.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
repr.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
tostring.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00
uint.lean chore(*): update equation syntax in files and old parser 2019-08-09 11:11:34 +02:00