Commit 2022-08-24 11:40 7c9da281

View on Github →

feat: Array.ofFn and lemmas (#381) This adds the Array.ofFn function which is analogous to List.ofFn as well as characterizing lemmas.

Estimated changes

added theorem Array.getElem_mapIdx
added theorem Array.getElem_ofFn
added theorem Array.size_mapIdx
added theorem Array.size_mapIdxM_Id
added theorem Array.size_mapIdxM_map
added theorem Array.size_mkEmpty
added theorem Array.size_ofFn
added theorem Array.size_ofFn_loop
added theorem Array.size_reverse
added theorem Array.size_reverse_rev
added theorem Array.size_swap!
added def Array.ofFn