mathlib documentation

data.buffer.parser.basic

Parsers #

parser α is the type that describes a computation that can ingest a char_buffer and output, if successful, a term of type α. This file expands on the definitions in the core library, proving that all the core library parsers are mono. There are also lemmas on the composability of parsers.

Main definitions #

Implementation details #

Lemmas about how parsers are mono are in the mono namespace. That allows using projection notation for shorter term proofs that are parallel to the definitions of the parsers in structure.

@[simp]
def parse_result.pos {α : Type} :

For some parse_result α, give the position at which the result was provided, in either the done or the fail case.

Equations
theorem parser.mono.le {α : Type} (p : parser α) (cb : char_buffer) (n : ) [p.mono] :
n (p cb n).pos
theorem parser.bounded.exists {α : Type} (p : parser α) [p.bounded] {cb : char_buffer} {n : } (h : buffer.size cb n) :
∃ (n' : ) (err : dlist string), p cb n = parse_result.fail n' err
@[class]
structure parser.conditionally_unfailing {α : Type} (p : parser α) :
Prop

A parser a is defined to be conditionally_unfailing if it produces a done parse_result as long as it is parsing within the provided char_buffer.

Instances
theorem parser.fail_iff {α : Type} (p : parser α) (cb : char_buffer) (n : ) :
(∀ (pos' : ) (result : α), p cb n parse_result.done pos' result) ∃ (pos' : ) (err : dlist string), p cb n = parse_result.fail pos' err
theorem parser.success_iff {α : Type} (p : parser α) (cb : char_buffer) (n : ) :
(∀ (pos' : ) (err : dlist string), p cb n parse_result.fail pos' err) ∃ (pos' : ) (result : α), p cb n = parse_result.done pos' result
theorem parser.mono.of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {a : α} [p.mono] (h : p cb n = parse_result.done n' a) :
n n'
theorem parser.mono.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [p.mono] (h : p cb n = parse_result.fail n' err) :
n n'
theorem parser.bounded.of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {a : α} [p.bounded] (h : p cb n = parse_result.done n' a) :
theorem parser.static.iff {α : Type} {p : parser α} :
p.static ∀ (cb : char_buffer) (n n' : ) (a : α), p cb n = parse_result.done n' an = n'
theorem parser.exists_done {α : Type} (p : parser α) [p.unfailing] (cb : char_buffer) (n : ) :
∃ (n' : ) (a : α), p cb n = parse_result.done n' a
theorem parser.unfailing.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [p.unfailing] (h : p cb n = parse_result.fail n' err) :
theorem parser.exists_done_in_bounds {α : Type} (p : parser α) [p.conditionally_unfailing] {cb : char_buffer} {n : } (h : n < buffer.size cb) :
∃ (n' : ) (a : α), p cb n = parse_result.done n' a
theorem parser.conditionally_unfailing.of_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [p.conditionally_unfailing] (h : p cb n = parse_result.fail n' err) (hn : n < buffer.size cb) :
theorem parser.decorate_errors_fail {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (h : p cb n = parse_result.fail n' err) :
theorem parser.decorate_errors_success {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {a : α} (h : p cb n = parse_result.done n' a) :
theorem parser.decorate_error_fail {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (h : p cb n = parse_result.fail n' err) :
parser.decorate_error msg p cb n = parse_result.fail n (dlist.lazy_of_list (λ («_» : unit), [msg ()]))
theorem parser.decorate_error_success {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {a : α} (h : p cb n = parse_result.done n' a) :
@[simp]
theorem parser.decorate_errors_eq_done {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {a : α} :
@[simp]
theorem parser.decorate_error_eq_done {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {a : α} :
@[simp]
theorem parser.decorate_errors_eq_fail {α : Type} {msgs : thunk (list string)} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} :
parser.decorate_errors msgs p cb n = parse_result.fail n' err n = n' err = dlist.lazy_of_list (λ («_» : unit), msgs ()) ∃ (np : ) (err' : dlist string), p cb n = parse_result.fail np err'
@[simp]
theorem parser.decorate_error_eq_fail {α : Type} {msg : thunk string} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} :
parser.decorate_error msg p cb n = parse_result.fail n' err n = n' err = dlist.lazy_of_list (λ («_» : unit), [msg ()]) ∃ (np : ) (err' : dlist string), p cb n = parse_result.fail np err'
@[simp]
theorem parser.return_eq_pure {α : Type} {a : α} :
theorem parser.pure_eq_done {α : Type} {a : α} :
pure a = λ (_x : char_buffer) (n : ), parse_result.done n a
@[simp]
theorem parser.pure_ne_fail {α : Type} {cb : char_buffer} {n n' : } {err : dlist string} {a : α} :
pure a cb n parse_result.fail n' err
@[simp]
theorem parser.bind_eq_bind {α β : Type} {p : parser α} (f : α → parser β) :
p.bind f = p >>= f
@[simp]
theorem parser.bind_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b : β} {f : α → parser β} :
(p >>= f) cb n = parse_result.done n' b ∃ (np : ) (a : α), p cb n = parse_result.done np a f a cb np = parse_result.done n' b
@[simp]
theorem parser.bind_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {f : α → parser β} :
(p >>= f) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a f a cb np = parse_result.fail n' err
@[simp]
theorem parser.and_then_eq_bind {α β : Type} {m : Type → Type} [monad m] (a : m α) (b : m β) :
a >> b = a >>= λ (_x : α), b
theorem parser.and_then_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} :
(p >> return ()) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
theorem parser.and_then_success {α : Type} {p : parser α} {cb : char_buffer} {n n' : } :
(p >> return ()) cb n = parse_result.done n' () ∃ (a : α), p cb n = parse_result.done n' a
@[simp]
theorem parser.map_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b : β} {f : α → β} :
(f <$> p) cb n = parse_result.done n' b ∃ (a : α), p cb n = parse_result.done n' a f a = b
@[simp]
theorem parser.map_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {f : α → β} :
(f <$> p) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
theorem parser.map_const_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b b' : β} :
(b <$ p) cb n = parse_result.done n' b' ∃ (a : α), p cb n = parse_result.done n' a b = b'
@[simp]
theorem parser.map_const_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {b : β} :
(b <$ p) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
theorem parser.map_const_rev_eq_done {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {b b' : β} :
(p $> b) cb n = parse_result.done n' b' ∃ (a : α), p cb n = parse_result.done n' a b = b'
theorem parser.map_rev_const_eq_fail {α β : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {b : β} :
(p $> b) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
theorem parser.orelse_eq_orelse {α : Type} {p q : parser α} :
p.orelse q = (p <|> q)
@[simp]
theorem parser.orelse_eq_done {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {a : α} :
(p <|> q) cb n = parse_result.done n' a p cb n = parse_result.done n' a q cb n = parse_result.done n' a ∃ (err : dlist string), p cb n = parse_result.fail n err
@[simp]
theorem parser.orelse_eq_fail_eq {α : Type} {p q : parser α} {cb : char_buffer} {n : } {err : dlist string} :
(p <|> q) cb n = parse_result.fail n err (p cb n = parse_result.fail n err ∃ (nq : ) (errq : dlist string), n < nq q cb n = parse_result.fail nq errq) ∃ (errp errq : dlist string), p cb n = parse_result.fail n errp q cb n = parse_result.fail n errq errp ++ errq = err
theorem parser.orelse_eq_fail_not_mono_lt {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {err : dlist string} (hn : n' < n) :
(p <|> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err q cb n = parse_result.fail n' err ∃ (errp : dlist string), p cb n = parse_result.fail n errp
theorem parser.orelse_eq_fail_of_mono_ne {α : Type} {p q : parser α} {cb : char_buffer} {n n' : } {err : dlist string} [q.mono] (hn : n n') :
(p <|> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err
@[simp]
@[simp]
theorem parser.failure_def {α : Type} {cb : char_buffer} {n : } :
theorem parser.not_failure_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} :
theorem parser.failure_eq_fail {α : Type} {cb : char_buffer} {n n' : } {err : dlist string} :
theorem parser.seq_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : parser (α → β)} {p : parser α} :
(f <*> p) cb n = parse_result.done n' b ∃ (nf : ) (f' : α → β) (a : α), f cb n = parse_result.done nf f' p cb nf = parse_result.done n' a f' a = b
theorem parser.seq_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {f : parser (α → β)} {p : parser α} :
(f <*> p) cb n = parse_result.fail n' err f cb n = parse_result.fail n' err ∃ (nf : ) (f' : α → β), f cb n = parse_result.done nf f' p cb nf = parse_result.fail n' err
theorem parser.seq_left_eq_done {α β : Type} {cb : char_buffer} {n n' : } {a : α} {p : parser α} {q : parser β} :
(p <* q) cb n = parse_result.done n' a ∃ (np : ) (b : β), p cb n = parse_result.done np a q cb np = parse_result.done n' b
theorem parser.seq_left_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {p : parser α} {q : parser β} :
(p <* q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.fail n' err
theorem parser.seq_right_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {p : parser α} {q : parser β} :
(p *> q) cb n = parse_result.done n' b ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.done n' b
theorem parser.seq_right_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {err : dlist string} {p : parser α} {q : parser β} :
(p *> q) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a q cb np = parse_result.fail n' err
theorem parser.mmap_eq_done {α β : Type} {cb : char_buffer} {n n' : } {f : α → parser β} {a : α} {l : list α} {b : β} {l' : list β} :
mmap f (a :: l) cb n = parse_result.done n' (b :: l') ∃ (np : ), f a cb n = parse_result.done np b mmap f l cb np = parse_result.done n' l'
theorem parser.mmap'_eq_done {α β : Type} {cb : char_buffer} {n n' : } {f : α → parser β} {a : α} {l : list α} :
mmap' f (a :: l) cb n = parse_result.done n' () ∃ (np : ) (b : β), f a cb n = parse_result.done np b mmap' f l cb np = parse_result.done n' ()
theorem parser.guard_eq_done {cb : char_buffer} {n n' : } {p : Prop} [decidable p] {u : unit} :
guard p cb n = parse_result.done n' u p n = n'
theorem parser.guard_eq_fail {cb : char_buffer} {n n' : } {err : dlist string} {p : Prop} [decidable p] :
guard p cb n = parse_result.fail n' err ¬p n = n' err = dlist.empty
@[instance]
def parser.mono.pure {α : Type} {a : α} :
@[instance]
def parser.mono.bind {α β : Type} {p : parser α} {f : α → parser β} [p.mono] [∀ (a : α), (f a).mono] :
(p >>= f).mono
@[instance]
def parser.mono.and_then {α β : Type} {p : parser α} {q : parser β} [p.mono] [q.mono] :
(p >> q).mono
@[instance]
def parser.mono.map {α β : Type} {p : parser α} [p.mono] {f : α → β} :
@[instance]
def parser.mono.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.mono] [p.mono] :
(f <*> p).mono
@[instance]
def parser.mono.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a l(f a).mono] :
(mmap f l).mono
@[instance]
def parser.mono.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), a l(f a).mono] :
(mmap' f l).mono
@[instance]
def parser.mono.failure {α : Type} :
@[instance]
def parser.mono.guard {p : Prop} [decidable p] :
@[instance]
def parser.mono.orelse {α : Type} {p q : parser α} [p.mono] [q.mono] :
(p <|> q).mono
@[instance]
def parser.mono.decorate_errors {α : Type} {msgs : thunk (list string)} {p : parser α} [p.mono] :
@[instance]
def parser.mono.decorate_error {α : Type} {msg : thunk string} {p : parser α} [p.mono] :
@[instance]
def parser.mono.sat {p : char → Prop} [decidable_pred p] :
@[instance]
@[instance]
def parser.mono.ch {c : char} :
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
def parser.mono.foldr_core {α β : Type} {p : parser α} {f : α → β → β} {b : β} [p.mono] {reps : } :
(parser.foldr_core f p b reps).mono
@[instance]
def parser.mono.foldr {α β : Type} {p : parser α} {b : β} {f : α → β → β} [p.mono] :
@[instance]
def parser.mono.foldl_core {α β : Type} {f : α → β → α} {p : parser β} [p.mono] {a : α} {reps : } :
(parser.foldl_core f a p reps).mono
@[instance]
def parser.mono.foldl {α β : Type} {a : α} {f : α → β → α} {p : parser β} [p.mono] :
@[instance]
def parser.mono.many {α : Type} {p : parser α} [p.mono] :
@[instance]
@[instance]
def parser.mono.many' {α : Type} {p : parser α} [p.mono] :
@[instance]
def parser.mono.many1 {α : Type} {p : parser α} [p.mono] :
@[instance]
@[instance]
def parser.mono.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.mono] [sep.mono] :
(sep.sep_by1 p).mono
@[instance]
def parser.mono.sep_by {α : Type} {p : parser α} {sep : parser unit} [p.mono] [hs : sep.mono] :
(sep.sep_by p).mono
theorem parser.mono.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.mono(F p).mono) (max_depth : ) :
(parser.fix_core F max_depth).mono
@[instance]
theorem parser.mono.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.mono(F p).mono) :
@[simp]
theorem parser.orelse_pure_eq_fail {α : Type} {p : parser α} {cb : char_buffer} {n n' : } {err : dlist string} {a : α} :
(p <|> pure a) cb n = parse_result.fail n' err p cb n = parse_result.fail n' err n n'
theorem parser.any_char_eq_done {cb : char_buffer} {n n' : } {c : char} :
parser.any_char cb n = parse_result.done n' c ∃ (hn : n < buffer.size cb), n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.sat_eq_done {cb : char_buffer} {n n' : } {c : char} {p : char → Prop} [decidable_pred p] :
parser.sat p cb n = parse_result.done n' c ∃ (hn : n < buffer.size cb), p c n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.sat_eq_fail {cb : char_buffer} {n n' : } {err : dlist string} {p : char → Prop} [decidable_pred p] :
parser.sat p cb n = parse_result.fail n' err n = n' err = dlist.empty ∀ (h : n < buffer.size cb), ¬p (buffer.read cb n, h⟩)
theorem parser.eps_eq_done {cb : char_buffer} {n n' : } {u : unit} :
theorem parser.ch_eq_done {cb : char_buffer} {n n' : } {c : char} {u : unit} :
parser.ch c cb n = parse_result.done n' u ∃ (hn : n < buffer.size cb), n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.one_of_eq_done {cb : char_buffer} {n n' : } {c : char} {cs : list char} :
parser.one_of cs cb n = parse_result.done n' c ∃ (hn : n < buffer.size cb), c cs n' = n + 1 buffer.read cb n, hn⟩ = c
theorem parser.one_of'_eq_done {cb : char_buffer} {n n' : } {u : unit} {cs : list char} :
parser.one_of' cs cb n = parse_result.done n' u ∃ (hn : n < buffer.size cb), buffer.read cb n, hn⟩ cs n' = n + 1
theorem parser.str_eq_done {cb : char_buffer} {n n' : } {u : unit} {s : string} :
theorem parser.eof_eq_done {cb : char_buffer} {n n' : } {u : unit} :
@[simp]
theorem parser.foldr_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {b' : β} :
theorem parser.foldr_core_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {reps : } {b' : β} :
parser.foldr_core f p b (reps + 1) cb n = parse_result.done n' b' (∃ (np : ) (a : α) (xs : β), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.done n' xs f a xs = b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.fail n err
@[simp]
theorem parser.foldr_core_zero_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} :
parser.foldr_core f p b 0 cb n = parse_result.fail n' err n = n' err = dlist.empty
theorem parser.foldr_core_succ_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {reps : } {err : dlist string} :
parser.foldr_core f p b (reps + 1) cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b reps cb np = parse_result.fail n' err)
theorem parser.foldr_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {b' : β} :
parser.foldr f p b cb n = parse_result.done n' b' (∃ (np : ) (a : α) (x : β), p cb n = parse_result.done np a parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.done n' x f a x = b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (x : α), p cb n = parse_result.done np x parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.foldr_eq_fail_iff_mono_at_end {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} [p.mono] (hc : buffer.size cb n) :
parser.foldr f p b cb n = parse_result.fail n' err n < n' (p cb n = parse_result.fail n' err ∃ (a : α), p cb n = parse_result.done n' a err = dlist.empty)
theorem parser.foldr_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : α → β → β} {p : parser α} {err : dlist string} :
parser.foldr f p b cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core f p b (buffer.size cb - n) cb np = parse_result.fail n' err)
@[simp]
theorem parser.foldl_core_zero_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {b' : β} :
theorem parser.foldl_core_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {reps : } {b' : β} :
parser.foldl_core f b p (reps + 1) cb n = parse_result.done n' b' (∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.done n' b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.fail n err
@[simp]
theorem parser.foldl_core_zero_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} :
parser.foldl_core f b p 0 cb n = parse_result.fail n' err n = n' err = dlist.empty
theorem parser.foldl_core_succ_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {reps : } {err : dlist string} :
parser.foldl_core f b p (reps + 1) cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p reps cb np = parse_result.fail n' err)
theorem parser.foldl_eq_done {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {b' : β} :
parser.foldl f b p cb n = parse_result.done n' b' (∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.done n' b') n = n' b = b' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.foldl_eq_fail {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} :
parser.foldl f b p cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldl_core f (f b a) p (buffer.size cb - n) cb np = parse_result.fail n' err)
theorem parser.foldl_eq_fail_iff_mono_at_end {α β : Type} {cb : char_buffer} {n n' : } {b : β} {f : β → α → β} {p : parser α} {err : dlist string} [p.mono] (hc : buffer.size cb n) :
parser.foldl f b p cb n = parse_result.fail n' err n < n' (p cb n = parse_result.fail n' err ∃ (a : α), p cb n = parse_result.done n' a err = dlist.empty)
theorem parser.many_eq_done_nil {α : Type} {cb : char_buffer} {n n' : } {p : parser α} :
p.many cb n = parse_result.done n' list.nil n = n' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.many_eq_done {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {x : α} {xs : list α} :
p.many cb n = parse_result.done n' (x :: xs) ∃ (np : ), p cb n = parse_result.done np x parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.done n' xs
theorem parser.many_eq_fail {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {err : dlist string} :
p.many cb n = parse_result.fail n' err n n' (p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n' err)
theorem parser.many_char_eq_done_empty {cb : char_buffer} {n n' : } {p : parser char} :
p.many_char cb n = parse_result.done n' "" n = n' ∃ (err : dlist string), p cb n = parse_result.fail n err ∃ (np : ) (c : char), p cb n = parse_result.done np c parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.fail n err
theorem parser.many'_eq_done {α : Type} {cb : char_buffer} {n n' : } {u : unit} {p : parser α} :
p.many' cb n = parse_result.done n' u p.many cb n = parse_result.done n' list.nil ∃ (np : ) (a : α) (l : list α), p.many cb n = parse_result.done n' (a :: l) p cb n = parse_result.done np a parser.foldr_core list.cons p list.nil (buffer.size cb - n) cb np = parse_result.done n' l
@[simp]
theorem parser.many1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : } {p : parser α} :
theorem parser.many1_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {p : parser α} {l : list α} :
p.many1 cb n = parse_result.done n' (a :: l) ∃ (np : ), p cb n = parse_result.done np a p.many cb np = parse_result.done n' l
theorem parser.many1_eq_fail {α : Type} {cb : char_buffer} {n n' : } {p : parser α} {err : dlist string} :
p.many1 cb n = parse_result.fail n' err p cb n = parse_result.fail n' err ∃ (np : ) (a : α), p cb n = parse_result.done np a p.many cb np = parse_result.fail n' err
@[simp]
theorem parser.many_char1_ne_empty {cb : char_buffer} {n n' : } {p : parser char} :
theorem parser.many_char1_eq_done {cb : char_buffer} {n n' : } {p : parser char} {s : string} (h : s "") :
p.many_char1 cb n = parse_result.done n' s ∃ (np : ), p cb n = parse_result.done np s.head p.many_char cb np = parse_result.done n' (s.popn 1)
@[simp]
theorem parser.sep_by1_ne_done_nil {α : Type} {cb : char_buffer} {n n' : } {sep : parser unit} {p : parser α} :
theorem parser.sep_by1_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {sep : parser unit} {p : parser α} {l : list α} :
sep.sep_by1 p cb n = parse_result.done n' (a :: l) ∃ (np : ), p cb n = parse_result.done np a (sep >> p).many cb np = parse_result.done n' l
theorem parser.sep_by_eq_done_nil {α : Type} {cb : char_buffer} {n n' : } {sep : parser unit} {p : parser α} :
sep.sep_by p cb n = parse_result.done n' list.nil n = n' ∃ (err : dlist string), sep.sep_by1 p cb n = parse_result.fail n err
@[simp]
theorem parser.fix_core_ne_done_zero {α : Type} {cb : char_buffer} {n n' : } {a : α} {F : parser αparser α} :
theorem parser.fix_core_eq_done {α : Type} {cb : char_buffer} {n n' : } {a : α} {F : parser αparser α} {max_depth : } :
parser.fix_core F (max_depth + 1) cb n = parse_result.done n' a F (parser.fix_core F max_depth) cb n = parse_result.done n' a
theorem parser.digit_eq_done {cb : char_buffer} {n n' k : } :
parser.digit cb n = parse_result.done n' k ∃ (hn : n < buffer.size cb), n' = n + 1 k 9 (buffer.read cb n, hn⟩).to_nat - '0'.to_nat = k '0' buffer.read cb n, hn⟩ buffer.read cb n, hn⟩ '9'
theorem parser.digit_eq_fail {cb : char_buffer} {n n' : } {err : dlist string} :
parser.digit cb n = parse_result.fail n' err n = n' err = dlist.of_list [""] ∀ (h : n < buffer.size cb), ¬(λ (c : char), '0' c c '9') (buffer.read cb n, h⟩)
theorem parser.static.not_of_ne {α : Type} {p : parser α} {cb : char_buffer} {n' n : } {a : α} (h : p cb n = parse_result.done n' a) (hne : n n') :
@[instance]
def parser.static.pure {α : Type} {a : α} :
@[instance]
def parser.static.bind {α β : Type} {p : parser α} {f : α → parser β} [p.static] [∀ (a : α), (f a).static] :
(p >>= f).static
@[instance]
def parser.static.and_then {α β : Type} {p : parser α} {q : parser β} [p.static] [q.static] :
(p >> q).static
@[instance]
def parser.static.map {α β : Type} {p : parser α} [p.static] {f : α → β} :
@[instance]
def parser.static.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [p.static] :
(f <*> p).static
@[instance]
def parser.static.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] :
(mmap f l).static
@[instance]
def parser.static.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] :
@[instance]
def parser.static.failure {α : Type} :
@[instance]
def parser.static.guard {p : Prop} [decidable p] :
@[instance]
def parser.static.orelse {α : Type} {p q : parser α} [p.static] [q.static] :
(p <|> q).static
@[instance]
def parser.static.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.static] :
@[instance]
def parser.static.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.static] :
theorem parser.static.sat_iff {p : char → Prop} [decidable_pred p] :
(parser.sat p).static ∀ (c : char), ¬p c
@[instance]
def parser.static.sat  :
(parser.sat (λ (_x : char), false)).static
@[instance]
def parser.static.foldr_core {α β : Type} {p : parser α} {f : α → β → β} [p.static] {b : β} {reps : } :
@[instance]
def parser.static.foldr {α β : Type} {p : parser α} {b : β} {f : α → β → β} [p.static] :
@[instance]
def parser.static.foldl_core {α β : Type} {f : α → β → α} {p : parser β} [p.static] {a : α} {reps : } :
@[instance]
def parser.static.foldl {α β : Type} {a : α} {f : α → β → α} {p : parser β} [p.static] :
@[instance]
def parser.static.many {α : Type} {p : parser α} [p.static] :
@[instance]
def parser.static.many' {α : Type} {p : parser α} [p.static] :
@[instance]
def parser.static.many1 {α : Type} {p : parser α} [p.static] :
@[instance]
def parser.static.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.static] [sep.static] :
(sep.sep_by1 p).static
@[instance]
def parser.static.sep_by {α : Type} {p : parser α} {sep : parser unit} [p.static] [sep.static] :
(sep.sep_by p).static
theorem parser.static.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.static(F p).static) (max_depth : ) :
(parser.fix_core F max_depth).static
theorem parser.static.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.static(F p).static) :
theorem parser.bounded.done_of_unbounded {α : Type} {p : parser α} (h : ¬p.bounded) :
∃ (cb : char_buffer) (n n' : ) (a : α), p cb n = parse_result.done n' a buffer.size cb n
theorem parser.bounded.pure {α : Type} {a : α} :
@[instance]
def parser.bounded.bind {α β : Type} {p : parser α} {f : α → parser β} [p.bounded] :
(p >>= f).bounded
@[instance]
def parser.bounded.and_then {α β : Type} {p : parser α} {q : parser β} [p.bounded] :
(p >> q).bounded
@[instance]
def parser.bounded.map {α β : Type} {p : parser α} [p.bounded] {f : α → β} :
@[instance]
def parser.bounded.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.bounded] :
(f <*> p).bounded
@[instance]
def parser.bounded.mmap {α β : Type} {a : α} {l : list α} {f : α → parser β} [∀ (a : α), (f a).bounded] :
(mmap f (a :: l)).bounded
@[instance]
def parser.bounded.mmap' {α β : Type} {a : α} {l : list α} {f : α → parser β} [∀ (a : α), (f a).bounded] :
(mmap' f (a :: l)).bounded
@[instance]
theorem parser.bounded.guard_iff {p : Prop} [decidable p] :
@[instance]
def parser.bounded.orelse {α : Type} {p q : parser α} [p.bounded] [q.bounded] :
(p <|> q).bounded
@[instance]
def parser.bounded.decorate_errors {α : Type} {msgs : thunk (list string)} {p : parser α} [p.bounded] :
@[instance]
def parser.bounded.decorate_error {α : Type} {msg : thunk string} {p : parser α} [p.bounded] :
@[instance]
def parser.bounded.sat {p : char → Prop} [decidable_pred p] :
@[instance]
@[instance]
@[instance]
@[instance]
def parser.bounded.foldr_core_zero {α β : Type} {p : parser α} {b : β} {f : α → β → β} :
@[instance]
def parser.bounded.foldl_core_zero {α β : Type} {p : parser α} {f : β → α → β} {b : β} :
theorem parser.bounded.foldr_core {α β : Type} {p : parser α} {b : β} {reps : } [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') {f : α → β → β} :
theorem parser.bounded.foldr {α β : Type} {p : parser α} {b : β} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') {f : α → β → β} :
theorem parser.bounded.foldl_core {α β : Type} {p : parser α} {b : β} {reps : } [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') {f : β → α → β} :
theorem parser.bounded.foldl {α β : Type} {p : parser α} {b : β} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') {f : β → α → β} :
theorem parser.bounded.many {α : Type} {p : parser α} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') :
theorem parser.bounded.many_char {pc : parser char} [pc.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), pc cb n = parse_result.fail n' errn n') :
theorem parser.bounded.many' {α : Type} {p : parser α} [hpb : p.bounded] (he : ∀ (cb : char_buffer) (n n' : ) (err : dlist string), p cb n = parse_result.fail n' errn n') :
@[instance]
def parser.bounded.many1 {α : Type} {p : parser α} [p.bounded] :
@[instance]
def parser.bounded.sep_by1 {α : Type} {p : parser α} {sep : parser unit} [p.bounded] :
theorem parser.bounded.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.bounded(F p).bounded) (max_depth : ) :
(parser.fix_core F max_depth).bounded
theorem parser.bounded.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.bounded(F p).bounded) :
theorem parser.unfailing.of_bounded {α : Type} {p : parser α} [p.bounded] :
@[instance]
def parser.unfailing.pure {α : Type} {a : α} :
@[instance]
def parser.unfailing.bind {α β : Type} {p : parser α} {f : α → parser β} [p.unfailing] [∀ (a : α), (f a).unfailing] :
@[instance]
def parser.unfailing.and_then {α β : Type} {p : parser α} {q : parser β} [p.unfailing] [q.unfailing] :
@[instance]
def parser.unfailing.map {α β : Type} {p : parser α} [p.unfailing] {f : α → β} :
@[instance]
def parser.unfailing.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.unfailing] [p.unfailing] :
@[instance]
def parser.unfailing.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] :
@[instance]
def parser.unfailing.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] :
@[instance]
def parser.unfailing.orelse {α : Type} {p q : parser α} [p.unfailing] :
@[instance]
@[instance]
theorem parser.unfailing.foldr_core_zero {α β : Type} {p : parser α} {f : α → β → β} {b : β} :
@[instance]
def parser.unfailing.foldr_core_of_static {α β : Type} {p : parser α} {f : α → β → β} {b : β} {reps : } [p.static] [p.unfailing] :
(parser.foldr_core f p b (reps + 1)).unfailing
@[instance]
def parser.unfailing.foldr_core_one_of_err_static {α β : Type} {p : parser α} {f : α → β → β} {b : β} [p.static] [p.err_static] :
theorem parser.err_static.not_of_ne {α : Type} {p : parser α} {cb : char_buffer} {n' n : } {err : dlist string} (h : p cb n = parse_result.fail n' err) (hne : n n') :
@[instance]
def parser.err_static.pure {α : Type} {a : α} :
@[instance]
def parser.err_static.bind {α β : Type} {p : parser α} {f : α → parser β} [p.static] [p.err_static] [∀ (a : α), (f a).err_static] :
@[instance]
def parser.err_static.bind_of_unfailing {α β : Type} {p : parser α} {f : α → parser β} [p.err_static] [∀ (a : α), (f a).unfailing] :
@[instance]
def parser.err_static.and_then {α β : Type} {p : parser α} {q : parser β} [p.static] [p.err_static] [q.err_static] :
@[instance]
def parser.err_static.and_then_of_unfailing {α β : Type} {p : parser α} {q : parser β} [p.err_static] [q.unfailing] :
@[instance]
def parser.err_static.map {α β : Type} {p : parser α} [p.err_static] {f : α → β} :
@[instance]
def parser.err_static.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [f.err_static] [p.err_static] :
@[instance]
def parser.err_static.seq_of_unfailing {α β : Type} {p : parser α} {f : parser (α → β)} [f.err_static] [p.unfailing] :
@[instance]
def parser.err_static.mmap {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] [∀ (a : α), (f a).err_static] :
@[instance]
def parser.err_static.mmap_of_unfailing {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] [∀ (a : α), (f a).err_static] :
@[instance]
def parser.err_static.mmap' {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).static] [∀ (a : α), (f a).err_static] :
@[instance]
def parser.err_static.mmap'_of_unfailing {α β : Type} {l : list α} {f : α → parser β} [∀ (a : α), (f a).unfailing] [∀ (a : α), (f a).err_static] :
@[instance]
@[instance]
@[instance]
def parser.err_static.orelse {α : Type} {p q : parser α} [p.err_static] [q.mono] :
@[instance]
@[instance]
@[instance]
@[instance]
theorem parser.err_static.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.err_static(F p).err_static) (max_depth : ) :
theorem parser.err_static.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.err_static(F p).err_static) :
theorem parser.step.not_step_of_static_done {α : Type} {p : parser α} [p.static] (h : ∃ (cb : char_buffer) (n n' : ) (a : α), p cb n = parse_result.done n' a) :
theorem parser.step.pure {α : Type} (a : α) :
@[instance]
def parser.step.bind {α β : Type} {p : parser α} {f : α → parser β} [p.step] [∀ (a : α), (f a).static] :
(p >>= f).step
@[instance]
def parser.step.bind' {α β : Type} {p : parser α} {f : α → parser β} [p.static] [∀ (a : α), (f a).step] :
(p >>= f).step
@[instance]
def parser.step.and_then {α β : Type} {p : parser α} {q : parser β} [p.step] [q.static] :
(p >> q).step
@[instance]
def parser.step.and_then' {α β : Type} {p : parser α} {q : parser β} [p.static] [q.step] :
(p >> q).step
@[instance]
def parser.step.map {α β : Type} {p : parser α} [p.step] {f : α → β} :
@[instance]
def parser.step.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.step] [p.static] :
(f <*> p).step
@[instance]
def parser.step.seq' {α β : Type} {p : parser α} {f : parser (α → β)} [f.static] [p.step] :
(f <*> p).step
@[instance]
def parser.step.mmap {α β : Type} {a : α} {f : α → parser β} [(f a).step] :
(mmap f [a]).step
@[instance]
def parser.step.mmap' {α β : Type} {a : α} {f : α → parser β} [(f a).step] :
(mmap' f [a]).step
@[instance]
def parser.step.failure {α : Type} :
@[instance]
@[instance]
def parser.step.orelse {α : Type} {p q : parser α} [p.step] [q.step] :
(p <|> q).step
theorem parser.step.decorate_errors_iff {α : Type} {p : parser α} {msgs : thunk (list string)} :
@[instance]
def parser.step.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.step] :
theorem parser.step.decorate_error_iff {α : Type} {p : parser α} {msg : thunk string} :
@[instance]
def parser.step.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.step] :
@[instance]
def parser.step.sat {p : char → Prop} [decidable_pred p] :
@[instance]
def parser.step.ch {c : char} :
@[instance]
@[instance]
theorem parser.step.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.step(F p).step) (max_depth : ) :
(parser.fix_core F max_depth).step
theorem parser.step.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.step(F p).step) :
theorem parser.many1_eq_done_iff_many_eq_done {α : Type} {p : parser α} {cb : char_buffer} {n' n : } [p.step] [p.bounded] {x : α} {xs : list α} :
p.many1 cb n = parse_result.done n' (x :: xs) p.many cb n = parse_result.done n' (x :: xs)
@[instance]
def parser.prog.of_step {α : Type} {p : parser α} [p.step] :
theorem parser.prog.pure {α : Type} (a : α) :
@[instance]
def parser.prog.bind {α β : Type} {p : parser α} {f : α → parser β} [p.prog] [∀ (a : α), (f a).mono] :
(p >>= f).prog
@[instance]
def parser.prog.and_then {α β : Type} {p : parser α} {q : parser β} [p.prog] [q.mono] :
(p >> q).prog
@[instance]
def parser.prog.map {α β : Type} {p : parser α} [p.prog] {f : α → β} :
@[instance]
def parser.prog.seq {α β : Type} {p : parser α} {f : parser (α → β)} [f.prog] [p.mono] :
(f <*> p).prog
@[instance]
def parser.prog.mmap {α β : Type} {a : α} {l : list α} {f : α → parser β} [(f a).prog] [∀ (a : α), (f a).mono] :
(mmap f (a :: l)).prog
@[instance]
def parser.prog.mmap' {α β : Type} {a : α} {l : list α} {f : α → parser β} [(f a).prog] [∀ (a : α), (f a).mono] :
(mmap' f (a :: l)).prog
@[instance]
def parser.prog.failure {α : Type} :
@[instance]
@[instance]
def parser.prog.orelse {α : Type} {p q : parser α} [p.prog] [q.prog] :
(p <|> q).prog
theorem parser.prog.decorate_errors_iff {α : Type} {p : parser α} {msgs : thunk (list string)} :
@[instance]
def parser.prog.decorate_errors {α : Type} {p : parser α} {msgs : thunk (list string)} [p.prog] :
theorem parser.prog.decorate_error_iff {α : Type} {p : parser α} {msg : thunk string} :
@[instance]
def parser.prog.decorate_error {α : Type} {p : parser α} {msg : thunk string} [p.prog] :
@[instance]
def parser.prog.sat {p : char → Prop} [decidable_pred p] :
@[instance]
def parser.prog.ch {c : char} :
@[instance]
@[instance]
theorem parser.prog.str_iff {s : string} :
@[instance]
def parser.prog.many1 {α : Type} {p : parser α} [p.mono] [p.prog] :
theorem parser.prog.fix_core {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.prog(F p).prog) (max_depth : ) :
(parser.fix_core F max_depth).prog
@[instance]
theorem parser.prog.fix {α : Type} {F : parser αparser α} (hF : ∀ (p : parser α), p.prog(F p).prog) :
theorem parser.many_sublist_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } [p.step] [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) (k : ) (H : k < n' - n) :
p.many cb (n + k) = parse_result.done n' (list.drop k l)
theorem parser.many_eq_nil_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } [p.step] [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) :
theorem parser.many_eq_nil_of_out_of_bound {α : Type} {p : parser α} {cb : char_buffer} {n n' : } [p.bounded] {l : list α} (h : p.many cb n = parse_result.done n' l) (hn : buffer.size cb < n) :
n' = n l = list.nil
theorem parser.many1_length_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } [p.mono] [p.step] [p.bounded] {l : list α} (h : p.many1 cb n = parse_result.done n' l) :
l.length = n' - n
theorem parser.many1_bounded_of_done {α : Type} {p : parser α} {cb : char_buffer} {n n' : } [p.step] [p.bounded] {l : list α} (h : p.many1 cb n = parse_result.done n' l) :
theorem parser.nat_of_done {cb : char_buffer} {n n' val : } (h : parser.nat cb n = parse_result.done n' val) :
val = nat.of_digits 10 (list.map (λ (c : char), c.to_nat - '0'.to_nat) (list.take (n' - n) (list.drop n (buffer.to_list cb))).reverse)

The val : ℕ produced by a successful parse of a cb : char_buffer is the numerical value represented by the string of decimal digits (possibly padded with 0s on the left) starting from the parsing position n and ending at position n'. The number of characters parsed in is necessarily n' - n.

This is one of the directions of nat_eq_done.

theorem parser.nat_of_done_as_digit {cb : char_buffer} {n n' val : } (h : parser.nat cb n = parse_result.done n' val) (hn : n' buffer.size cb) (k : ) (hk : k < n') :
n k'0' buffer.read cb k, _⟩ buffer.read cb k, _⟩ '9'

If we know that parser.nat was successful, starting at position n and ending at position n', then it must be the case that for all k : ℕ, n ≤ k, k < n', the character at the kth position in cb : char_buffer is "numeric", that is, is between '0' and '9' inclusive.

This is a necessary part of proving one of the directions of nat_eq_done.

theorem parser.nat_of_done_bounded {cb : char_buffer} {n n' val : } (h : parser.nat cb n = parse_result.done n' val) (hn : n' < buffer.size cb) :
'0' buffer.read cb n', hn⟩'9' < buffer.read cb n', hn⟩

If we know that parser.nat was successful, starting at position n and ending at position n', then it must be the case that for the ending position n', either it is beyond the end of the cb : char_buffer, or the character at that position is not "numeric", that is, between '0' and '9' inclusive.

This is a necessary part of proving one of the directions of nat_eq_done.

theorem parser.nat_eq_done {cb : char_buffer} {n n' val : } :
parser.nat cb n = parse_result.done n' val ∃ (hn : n < n'), val = nat.of_digits 10 (list.map (λ (c : char), c.to_nat - '0'.to_nat) (list.take (n' - n) (list.drop n (buffer.to_list cb))).reverse) (∀ (hn' : n' < buffer.size cb), '0' buffer.read cb n', hn'⟩'9' < buffer.read cb n', hn'⟩) ∃ (hn'' : n' buffer.size cb), ∀ (k : ) (hk : k < n'), n k'0' buffer.read cb k, _⟩ buffer.read cb k, _⟩ '9'

The val : ℕ produced by a successful parse of a cb : char_buffer is the numerical value represented by the string of decimal digits (possibly padded with 0s on the left) starting from the parsing position n and ending at position n', where n < n'. The number of characters parsed in is necessarily n' - n. Additionally, all of the characters in the cb starting at position n (inclusive) up to position n' (exclusive) are "numeric", in that they are between '0' and '9' inclusive. Such a char_buffer would produce the value encoded by its decimal characters.