c58f61e925
See discussion at #1438 https://github.com/leanprover/lean/pull/1438#discussion_r105007325 @digama0 With this commit, the original `array_list.write` will also perform a destructive update when the reference counter for `l` is 1. ```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α := λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v } ``` |
||
|---|---|---|
| .. | ||
| api | ||
| checker | ||
| cmake | ||
| emacs | ||
| frontends | ||
| init | ||
| kernel | ||
| library | ||
| shared | ||
| shell | ||
| tests | ||
| util | ||
| vim | ||
| CMakeLists.txt | ||
| CTestConfig.cmake | ||
| CTestCustom.cmake.in | ||
| Doxyfile | ||
| githash.h.in | ||
| memcheck.supp | ||
| version.h.in | ||