Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-23 14:09 8d3efb71

View on Github →

feat(data/buffer/basic): read and to_buffer lemmas (#6048)

Estimated changes

Modified src/data/array/lemmas.lean

added theorem array.read_push_back_left

added theorem array.read_push_back_right

Modified src/data/buffer/basic.lean

added theorem buffer.append_list_nil

added theorem buffer.length_to_list

added theorem buffer.read_append_list_left'

added theorem buffer.read_append_list_left

added theorem buffer.read_append_list_right

added theorem buffer.read_push_back_left

added theorem buffer.read_push_back_right

added theorem buffer.read_singleton

added theorem buffer.read_to_buffer'

added theorem buffer.read_to_buffer

added theorem buffer.size_append_list

added theorem buffer.size_push_back

added theorem buffer.size_singleton

added theorem buffer.size_to_buffer

added theorem buffer.to_buffer_cons

added theorem buffer.to_buffer_to_list

added theorem buffer.to_list_to_buffer