Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-06 20:09 a1ebf540

View on Github →

refactor(data/buffer/parser/basic): make valid a class and rename to mono (#6015)

Estimated changes

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

added theorem parser.foldl_eq_fail_iff_mono_at_end

added theorem parser.foldr_eq_fail_iff_mono_at_end

deleted theorem parser.foldr_eq_fail_of_valid_at_end

added theorem parser.mono.fix

added theorem parser.mono.fix_core

added theorem parser.mono.le

added theorem parser.mono.of_done

added theorem parser.mono.of_fail

deleted theorem parser.orelse_eq_fail_invalid_lt

added theorem parser.orelse_eq_fail_not_mono_lt

added theorem parser.orelse_eq_fail_of_mono_ne

deleted theorem parser.orelse_eq_fail_of_valid_ne

deleted theorem parser.valid.and_then

deleted theorem parser.valid.any_char

deleted theorem parser.valid.bind

deleted theorem parser.valid.ch

deleted theorem parser.valid.char_buf

deleted theorem parser.valid.decorate_error

deleted theorem parser.valid.decorate_errors

deleted theorem parser.valid.digit

deleted theorem parser.valid.eof

deleted theorem parser.valid.eps

deleted theorem parser.valid.failure

deleted theorem parser.valid.fix

deleted theorem parser.valid.fix_core

deleted theorem parser.valid.foldl

deleted theorem parser.valid.foldl_core

deleted theorem parser.valid.foldl_core_zero

deleted theorem parser.valid.foldr

deleted theorem parser.valid.foldr_core

deleted theorem parser.valid.foldr_core_zero

deleted theorem parser.valid.guard

deleted theorem parser.valid.many'

deleted theorem parser.valid.many1

deleted theorem parser.valid.many

deleted theorem parser.valid.many_char1

deleted theorem parser.valid.many_char

deleted theorem parser.valid.map

deleted theorem parser.valid.mmap'

deleted theorem parser.valid.mmap

deleted theorem parser.valid.mono_done

deleted theorem parser.valid.mono_fail

deleted theorem parser.valid.nat

deleted theorem parser.valid.one_of'

deleted theorem parser.valid.one_of

deleted theorem parser.valid.orelse

deleted theorem parser.valid.pure

deleted theorem parser.valid.remaining

deleted theorem parser.valid.sat

deleted theorem parser.valid.sep_by1

deleted theorem parser.valid.sep_by

deleted theorem parser.valid.seq

deleted theorem parser.valid.str

deleted def parser.valid