feat: arrays (#159)

Closes #91

Author: david-christiansen

Manual.lean

@@ -153,7 +153,7 @@ file := some "the-index"
 
 :::progress
 ```namespace
-String Char Nat Lean.Elab.Tactic
+String Char Nat Lean.Elab.Tactic Array Subarray
 ```
 ```exceptions
 String.revFindAux String.extract.go₂ String.substrEq.loop String.casesOn
@@ -223,6 +223,153 @@ Nat.le.below.refl
 Nat.le.below.casesOn
 ```
 
+```exceptions
+Array.get?_size
+Array.forIn'.loop
+Array.mapM.map
+Array.findIdx?.loop
+Array.get_extract_loop_lt
+Array.foldrM_eq_foldrM_data
+Array.get?_push
+Array.appendList_data
+Array.insertAt.loop
+Array.reverse.loop
+Array.foldrM_eq_reverse_foldlM_data
+Array.isPrefixOfAux
+Array.takeWhile.go
+Array.isPrefixOfAux
+Array.size_eq_length_data
+Array.qpartition.loop
+Array.insertionSort.swapLoop
+Array.foldl_data_eq_bind
+Array.foldl_toList_eq_bind
+Array.foldrMUnsafe
+Array.get_swap_left
+Array.get_extract_loop_ge_aux
+Array.data_swap
+Array.get_extract_loop_lt_aux
+Array.get?_swap
+Array.get_swap'
+Array.mapM_eq_mapM_data
+Array.anyM.loop
+Array.getElem_eq_data_getElem
+Array.get_swap_right
+Array.get_extract_loop_ge
+Array.foldrM.fold
+Array.foldlM.loop
+Array.take.loop
+Array.mapMUnsafe
+Array.binSearchAux
+Array.eq_push_pop_back_of_size_ne_zero
+Array.get?_push_eq
+Array.append_data
+Array.indexOfAux
+Array.reverse_toList
+Array.ofFn.go
+Array.get?_eq_data_get?
+Array.filterMap_data
+Array.empty_data
+Array.foldrMUnsafe.fold
+Array.toListImpl
+Array.filter_data
+Array.get_swap_of_ne
+Array.get_append_right
+Array.getElem?_eq_toList_getElem?
+Array.foldl_eq_foldl_data
+Array.sequenceMap.loop
+Array.toList_eq
+Array.findSomeRevM?.find
+Array.data_range
+Array.forIn'Unsafe.loop
+Array.foldlM_eq_foldlM_data
+Array.getElem_eq_toList_getElem
+Array.getElem_mem_data
+Array.get_extract
+Array.extract.loop
+Array.foldlMUnsafe.fold
+Array.data_set
+Array.forIn'Unsafe
+Array.mapMUnsafe.map
+Array.mapM'.go
+Array.pop_data
+Array.appendCore.loop
+Array.get?_len_le
+Array.back_push
+Array.all_def
+Array.get_push_lt
+Array.foldl_data_eq_map
+Array.get?_eq_toList_get?
+Array.isEqvAux
+Array.getElem?_mem
+Array.getElem_fin_eq_toList_get
+Array.getElem?_eq_data_get?
+Array.foldr_eq_foldr_data
+Array.data_length
+Array.get_push
+Array.push_data
+Array.toArray_data
+Array.get_append_left
+Array.insertionSort.traverse
+Array.getElem_fin_eq_data_get
+Array.toListLitAux
+Array.map_data
+Array.get?_push_lt
+Array.get_extract_aux
+Array.foldlMUnsafe
+Array.qsort.sort
+Array.any_def
+Array.anyMUnsafe
+Array.data_toArray
+Array.mem_data
+Array.get_swap
+Array.mapFinIdxM.map
+Array.data_pop
+Array.anyMUnsafe.any
+Array.mkArray0
+Array.mkArray1
+Array.mkArray2
+Array.mkArray3
+Array.mkArray4
+Array.mkArray5
+Array.mkArray6
+Array.mkArray7
+Array.mkArray8
+Array.mkEmpty
+Array.get_push_eq
+Array.appendCore
+Array.modifyMUnsafe
+Array.mapSepElems
+Array.mapSepElemsM
+Array.toArrayLit
+Array.getSepElems
+Array.zipWithAux
+Array.casesOn
+Array.rec
+Array.recOn
+Array.noConfusion
+Array.noConfusionType
+Array.tacticArray_get_dec
+Array.back_eq_back?
+Array.mkArray_data
+Array.getLit
+```
+
+```exceptions
+Array.qpartition
+```
+
+```exceptions
+Subarray.forInUnsafe.loop
+Subarray.as
+Subarray.casesOn
+Subarray.recOn
+Subarray.rec
+Subarray.noConfusion
+Subarray.noConfusionType
+Subarray.forInUnsafe
+Subarray.findSomeRevM?.find
+```
+
 ```exceptions
 Lean.Elab.Tactic.evalUnfold.go
 Lean.Elab.Tactic.dsimpLocation.go

Manual/BasicTypes.lean

@@ -9,6 +9,7 @@ import VersoManual
 import Manual.Meta
 import Manual.BasicTypes.Nat
 import Manual.BasicTypes.String
+import Manual.BasicTypes.Array
 
 open Manual.FFIDocType
 
@@ -142,17 +143,8 @@ tag := "List"
  * Constructor/pattern syntax
 :::
 
-# Arrays
-%%%
-tag := "Array"
-%%%
 
-::: planned 91
-Description and API reference for {name}`Thunk`:
- * Logical model as wrapper around a function from {lean}`Unit`
- * Run-time realization as a lazy computation
- * API reference
-:::
+{include 0 Manual.BasicTypes.Array}
 
 
 # Lazy Computations