Commit 2022-09-15 13:39 456b9f6b

View on Github →

chore: bump to 2022-09-15 (#414)

Estimated changes

deleted theorem List.Pairwise_cons
deleted theorem List.cons_union
deleted theorem List.disjoint_append_left
deleted theorem List.disjoint_comm
deleted theorem List.disjoint_cons_left
deleted theorem List.disjoint_iff_ne
deleted theorem List.disjoint_left
deleted theorem List.disjoint_nil_left
deleted theorem List.disjoint_nil_right
deleted theorem List.disjoint_right
deleted theorem List.disjoint_singleton
deleted theorem List.disjoint_symm
deleted theorem List.erase_append_left
deleted theorem List.erase_append_right
deleted theorem List.erase_cons
deleted theorem List.erase_cons_head
deleted theorem List.erase_cons_tail
deleted theorem List.erase_eq_erasep
deleted theorem List.erase_nil
deleted theorem List.erase_of_not_mem
deleted theorem List.erase_subset
deleted theorem List.erasep_append_left
deleted theorem List.erasep_append_right
deleted theorem List.erasep_cons
deleted theorem List.erasep_cons_of_neg
deleted theorem List.erasep_cons_of_pos
deleted theorem List.erasep_map
deleted theorem List.erasep_nil
deleted theorem List.erasep_of_forall_not
deleted theorem List.erasep_subset
deleted theorem List.exists_erase_eq
deleted theorem List.exists_of_erasep
deleted theorem List.ext
deleted theorem List.ext_get
deleted theorem List.get?_append
deleted theorem List.get?_append_right
deleted theorem List.get?_concat_length
deleted theorem List.get?_map
deleted theorem List.get?_modifyNth
deleted theorem List.get?_modifyNth_eq
deleted theorem List.get?_modifyNth_ne
deleted theorem List.get?_set_eq
deleted theorem List.get?_set_ne
deleted theorem List.get?_set_of_lt
deleted theorem List.getLast_eq_get
deleted theorem List.get_append
deleted theorem List.get_append_right'
deleted theorem List.get_append_right_aux
deleted theorem List.get_cons_length
deleted theorem List.get_map
deleted theorem List.get_of_eq
deleted theorem List.get_replicate
deleted theorem List.get_set_eq
deleted theorem List.get_set_ne
deleted theorem List.get_singleton
deleted theorem List.get_zero
deleted theorem List.insert_of_mem
deleted theorem List.insert_of_not_mem
deleted def List.leftpad
deleted theorem List.leftpad_length
deleted theorem List.leftpad_prefix
deleted theorem List.leftpad_suffix
deleted theorem List.length_erase_of_mem
deleted theorem List.length_erasep_of_mem
deleted theorem List.length_insert_of_mem
deleted theorem List.mem_erase_of_ne
deleted theorem List.mem_erasep_of_neg
deleted theorem List.mem_insert_iff
deleted theorem List.mem_insert_of_mem
deleted theorem List.mem_insert_self
deleted theorem List.mem_inter_iff
deleted theorem List.mem_of_mem_erase
deleted theorem List.mem_of_mem_erasep
deleted theorem List.mem_or_eq_of_mem_set
deleted theorem List.mem_union_iff
deleted theorem List.modifyNthTail_id
deleted theorem List.modifyNthTail_length
deleted theorem List.modifyNth_eq_set
deleted theorem List.modify_get?_length
deleted theorem List.nil_union
deleted theorem List.set_comm
deleted theorem List.set_eq_modifyNth
deleted theorem List.set_nil
deleted theorem List.set_succ
deleted theorem List.singleton_disjoint
modified theorem List.card_union_disjoint
deleted theorem Option.ball_ne_none
deleted theorem Option.bex_ne_none
deleted theorem Option.bind_assoc
deleted theorem Option.bind_comm
deleted theorem Option.bind_eq_none
deleted theorem Option.bind_eq_some
deleted theorem Option.bind_id_eq_join
deleted theorem Option.bind_map_comm
deleted theorem Option.bind_some
deleted theorem Option.choice_eq
deleted theorem Option.comp_map
deleted theorem Option.elim_none
deleted theorem Option.elim_some
deleted theorem Option.eq_some_iff_get_eq
deleted theorem Option.ext
deleted theorem Option.getD_map
deleted theorem Option.getD_none
deleted theorem Option.getD_of_ne_none
deleted theorem Option.getD_some
deleted theorem Option.get_mem
deleted theorem Option.get_of_mem
deleted theorem Option.get_some
deleted theorem Option.guard_eq_some
deleted theorem Option.isNone_none
deleted theorem Option.isNone_some
deleted theorem Option.isSome_iff_exists
deleted theorem Option.isSome_none
deleted theorem Option.isSome_some
deleted theorem Option.join_eq_some
deleted theorem Option.join_join
deleted theorem Option.join_ne_none'
deleted theorem Option.join_ne_none
deleted theorem Option.map_comp_map
deleted theorem Option.map_congr
deleted theorem Option.map_eq_map
deleted theorem Option.map_eq_none'
deleted theorem Option.map_eq_none
deleted theorem Option.map_eq_some'
deleted theorem Option.map_eq_some
deleted theorem Option.map_id'
deleted theorem Option.map_map
deleted theorem Option.map_none'
deleted theorem Option.map_none
deleted theorem Option.map_some'
deleted theorem Option.map_some
deleted theorem Option.mem_map_of_mem
deleted theorem Option.mem_of_mem_join
deleted theorem Option.mem_unique
deleted theorem Option.ne_none_iff_exists
deleted theorem Option.ne_none_iff_isSome
deleted theorem Option.none_bind
deleted theorem Option.none_orelse
deleted theorem Option.not_isSome
deleted theorem Option.not_mem_none
deleted theorem Option.orelse_none
deleted theorem Option.some_bind
deleted theorem Option.some_get
deleted theorem Option.some_ne_none
deleted theorem Option.some_orelse
deleted theorem Option.to_list_none
deleted theorem Option.to_list_some
deleted def Option.guard
deleted theorem Option.isNone_iff_eq_none
deleted def Option.join
deleted theorem Option.mem_def
deleted theorem Option.mem_iff
deleted def Option.pbind
deleted def Option.pmap
deleted theorem Option.some_inj
deleted def Option.toList
deleted def Option.get