max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/data/array
History
Rob Dockins a9ebf23fab fix(libraray/init/data): generalize universe variables in array and persistent array operations 
This change allows the monadic traversal operations on arrays to use monads that
are defined to raise universe levels.  This happens, for example, when defining
monads using certain continuation-passing idioms.
2019-07-11 17:52:04 -07:00
..
basic.lean fix(libraray/init/data): generalize universe variables in array and persistent array operations 2019-07-11 17:52:04 -07:00
binsearch.lean feat(frontends/lean): allow ; instead of in in let-decls 2019-06-27 17:12:03 -07:00
default.lean feat(library/init/data/array): add Array.binSearch 2019-05-14 18:25:54 -07:00
qsort.lean feat(frontends/lean): allow ; instead of in in let-decls 2019-06-27 17:12:03 -07:00