Commit 2022-12-12 18:44 16190b75

View on Github →

feat: port Data.Vector from lean-core (#834) Have also added some needed lemmas for Lists; from e574b1a4e891376b0ef974b926da39e05da12a06

Estimated changes

added def Vector.append
added def Vector.cons
added theorem Vector.cons_head_tail
added def Vector.drop
added def Vector.elim
added def Vector.head
added theorem Vector.head_cons
added def Vector.length
added def Vector.map
added def Vector.mapAccumr
added theorem Vector.map_cons
added theorem Vector.map_nil
added def Vector.map₂
added def Vector.nil
added def Vector.nth
added def Vector.ofFn
added def Vector.removeNth
added def Vector.tail
added theorem Vector.tail_cons
added def Vector.take
added def Vector.toList
added theorem Vector.toList_mk
added theorem Vector.to_list_append
added theorem Vector.to_list_cons
added theorem Vector.to_list_drop
added theorem Vector.to_list_length
added theorem Vector.to_list_nil
added theorem Vector.to_list_take
added def Vector
added def List.band
added def List.bor
added def List.findIndex
added def List.ilast
added def List.init
added def List.last
added theorem List.le_eq_not_gt
added def List.map₂
added def List.nth
added def List.nthLe
added def List.updateNth
added def List.«repeat»
added theorem List.length_mapAccumr
added theorem List.length_map₂
added theorem List.length_repeat
added def List.mapAccumr