Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-12 19:31 0e7a9214

View on Github →

feat(data/buffer/parser/basic): lemmas describing parsers (#5460)

Estimated changes

Created src/data/buffer/parser/basic.lean

added theorem exists_eq_right_right'

added theorem exists_eq_right_right

added theorem nat.le_of_sub_eq_pos

added theorem ne_iff_lt_iff_le

added def parse_result.pos

added theorem parser.and_then_eq_bind

added theorem parser.and_then_fail

added theorem parser.and_then_success

added theorem parser.any_char_eq_done

added theorem parser.bind_eq_bind

added theorem parser.bind_eq_done

added theorem parser.bind_eq_fail

added theorem parser.ch_eq_done

added theorem parser.decorate_error_eq_done

added theorem parser.decorate_error_eq_fail

added theorem parser.decorate_error_fail

added theorem parser.decorate_error_success

added theorem parser.decorate_errors_eq_done

added theorem parser.decorate_errors_eq_fail

added theorem parser.decorate_errors_fail

added theorem parser.decorate_errors_success

added theorem parser.digit_eq_done

added theorem parser.eof_eq_done

added theorem parser.eps_eq_done

added theorem parser.fail_iff

added theorem parser.failure_def

added theorem parser.failure_eq_fail

added theorem parser.failure_eq_failure

added theorem parser.fix_core_eq_done

added theorem parser.fix_core_ne_done_zero

added theorem parser.foldl_core_eq_done

added theorem parser.foldl_core_succ_eq_fail

added theorem parser.foldl_core_zero_eq_done

added theorem parser.foldl_core_zero_eq_fail

added theorem parser.foldl_eq_done

added theorem parser.foldl_eq_fail

added theorem parser.foldr_core_eq_done

added theorem parser.foldr_core_succ_eq_fail

added theorem parser.foldr_core_zero_eq_done

added theorem parser.foldr_core_zero_eq_fail

added theorem parser.foldr_eq_done

added theorem parser.foldr_eq_fail

added theorem parser.foldr_eq_fail_of_valid_at_end

added theorem parser.guard_eq_done

added theorem parser.guard_eq_fail

added theorem parser.many'_eq_done

added theorem parser.many1_eq_done

added theorem parser.many1_eq_fail

added theorem parser.many1_ne_done_nil

added theorem parser.many_char1_eq_done

added theorem parser.many_char1_ne_empty

added theorem parser.many_char_eq_done_empty

added theorem parser.many_char_eq_done_not_empty

added theorem parser.many_char_eq_many_of_to_list

added theorem parser.many_eq_done

added theorem parser.many_eq_done_nil

added theorem parser.many_eq_fail

added theorem parser.map_const_eq_done

added theorem parser.map_const_eq_fail

added theorem parser.map_const_rev_eq_done

added theorem parser.map_eq_done

added theorem parser.map_eq_fail

added theorem parser.map_rev_const_eq_fail

added theorem parser.mmap'_eq_done

added theorem parser.mmap_eq_done

added theorem parser.not_failure_eq_done

added theorem parser.one_of'_eq_done

added theorem parser.one_of_eq_done

added theorem parser.orelse_eq_done

added theorem parser.orelse_eq_fail_eq

added theorem parser.orelse_eq_fail_invalid_lt

added theorem parser.orelse_eq_fail_of_valid_ne

added theorem parser.orelse_eq_orelse

added theorem parser.orelse_pure_eq_fail

added theorem parser.pure_eq_done

added theorem parser.pure_ne_fail

added theorem parser.remaining_eq_done

added theorem parser.return_eq_pure

added theorem parser.sat_eq_done

added theorem parser.sep_by1_eq_done

added theorem parser.sep_by1_ne_done_nil

added theorem parser.sep_by_eq_done_nil

added theorem parser.seq_eq_done

added theorem parser.seq_eq_fail

added theorem parser.seq_left_eq_done

added theorem parser.seq_left_eq_fail

added theorem parser.seq_right_eq_done

added theorem parser.seq_right_eq_fail

added theorem parser.success_iff

added theorem parser.valid.and_then

added theorem parser.valid.any_char

added theorem parser.valid.bind

added theorem parser.valid.ch

added theorem parser.valid.char_buf

added theorem parser.valid.decorate_error

added theorem parser.valid.decorate_errors

added theorem parser.valid.digit

added theorem parser.valid.eof

added theorem parser.valid.eps

added theorem parser.valid.failure

added theorem parser.valid.fix

added theorem parser.valid.fix_core

added theorem parser.valid.foldl

added theorem parser.valid.foldl_core

added theorem parser.valid.foldl_core_zero

added theorem parser.valid.foldr

added theorem parser.valid.foldr_core

added theorem parser.valid.foldr_core_zero

added theorem parser.valid.guard

added theorem parser.valid.many'

added theorem parser.valid.many1

added theorem parser.valid.many

added theorem parser.valid.many_char1

added theorem parser.valid.many_char

added theorem parser.valid.map

added theorem parser.valid.mmap'

added theorem parser.valid.mmap

added theorem parser.valid.mono_done

added theorem parser.valid.mono_fail

added theorem parser.valid.nat

added theorem parser.valid.one_of'

added theorem parser.valid.one_of

added theorem parser.valid.orelse

added theorem parser.valid.pure

added theorem parser.valid.remaining

added theorem parser.valid.sat

added theorem parser.valid.sep_by1

added theorem parser.valid.sep_by

added theorem parser.valid.seq

added theorem parser.valid.str

added def parser.valid

Modified src/data/string/basic.lean

added theorem list.as_string_eq

added theorem list.as_string_inj

added theorem list.to_list_inv_as_string

added theorem string.as_string_inv_to_list

added theorem string.head_empty

added theorem string.nil_as_string_eq_empty

added theorem string.popn_empty

added theorem string.to_list_empty

added theorem string.to_list_nonempty

added theorem string.to_list_singleton

Modified src/data/string/defs.lean

added def string.head