Commit 2023-01-19 10:14 d9338095

View on Github →

Feat: Port/data.vector.basic (#1633) Port of data.vector.basic Does a realignment of Vector functions to mirror the List equivalents, particularly for nth which has been replaced by get

Estimated changes

added def Vector.get
deleted def Vector.nth
added theorem Vector.cons_val
added theorem Vector.eq_cons_iff
added theorem Vector.exists_eq_cons
added theorem Vector.ext
added theorem Vector.get_cons_nil
added theorem Vector.get_cons_succ
added theorem Vector.get_cons_zero
added theorem Vector.get_eq_get
added theorem Vector.get_map
added theorem Vector.get_ofFn
added theorem Vector.get_replicate
added theorem Vector.get_set_eq_if
added theorem Vector.get_set_of_ne
added theorem Vector.get_set_same
added theorem Vector.get_tail
added theorem Vector.get_tail_succ
added theorem Vector.get_zero
added theorem Vector.head?_toList
added theorem Vector.head_map
added theorem Vector.head_ofFn
added def Vector.insertNth
added theorem Vector.insertNth_comm
added theorem Vector.insertNth_val
added def Vector.last
added theorem Vector.last_def
added theorem Vector.length_val
added def Vector.mOfFn
added theorem Vector.mOfFn_pure
added theorem Vector.map_id
added theorem Vector.mk_toList
added def Vector.mmap
added theorem Vector.mmap_cons
added theorem Vector.mmap_nil
added theorem Vector.ne_cons_iff
added theorem Vector.nth_eq_nth_le
added theorem Vector.ofFn_get
added theorem Vector.prod_set'
added theorem Vector.prod_set
added theorem Vector.removeNth_val
added def Vector.reverse
added theorem Vector.reverse_reverse
added def Vector.scanl
added theorem Vector.scanl_cons
added theorem Vector.scanl_get
added theorem Vector.scanl_head
added theorem Vector.scanl_nil
added theorem Vector.scanl_singleton
added theorem Vector.scanl_val
added def Vector.set
added theorem Vector.singleton_tail
added theorem Vector.tail_map
added theorem Vector.tail_nil
added theorem Vector.tail_ofFn
added theorem Vector.tail_val
added def Vector.toArray
added theorem Vector.toList_empty
added theorem Vector.toList_map
added theorem Vector.toList_ofFn
added theorem Vector.toList_reverse
added theorem Vector.toList_scanl
added theorem Vector.toList_set