From 613b6805b34d86535115659de75aa815e7239d5d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 Jun 2018 14:25:58 +0200 Subject: [PATCH] chore(library/init/lean/parser/parser_t.lean): fix comments --- library/init/lean/parser/parser_t.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/init/lean/parser/parser_t.lean b/library/init/lean/parser/parser_t.lean index f9e6c4f0a4..687a1df54f 100644 --- a/library/init/lean/parser/parser_t.lean +++ b/library/init/lean/parser/parser_t.lean @@ -237,8 +237,8 @@ private def str_aux (s : string) : nat → iterator → iterator → result stri /-- `str s` parses a sequence of elements that match `s`. Returns the parsed string (i.e. `s`). -This parser_t m consumes no input if it fails (even if a partial match). -Note: The behaviour of this parser_t m is different to that the `string` parser_t m in the Parsec Haskell library, +This parser consumes no input if it fails (even if a partial match). +Note: The behaviour of this parser is different to that the `string` parser in the Parsec Haskell library, as this one is all-or-nothing. -/ def str (s : string) : parser_t m string := @@ -270,7 +270,7 @@ private def take_while_aux (p : char → bool) : nat → string → iterator → /-- Consume input as long as the predicate returns `tt`, and return the consumed input. -This parser_t m does not fail. It will return an empty string if the predicate +This parser does not fail. It will return an empty string if the predicate returns `ff` on the current character. -/ def take_while (p : char → bool) : parser_t m string := λ it, pure $ take_while_aux p it.remaining "" it @@ -280,7 +280,7 @@ def take_while_cont (p : char → bool) (ini : string) : parser_t m string := /-- Consume input as long as the predicate returns `tt`, and return the consumed input. -This parser_t m requires the predicate to succeed on at least once. -/ +This parser requires the predicate to succeed on at least once. -/ def take_while1 (p : char → bool) : parser_t m string := λ it, pure $ if !it.has_next then eoi_error it.offset @@ -292,7 +292,7 @@ def take_while1 (p : char → bool) : parser_t m string := /-- Consume input as long as the predicate returns `ff` (i.e. until it returns `tt`), and return the consumed input. -This parser_t m does not fail. -/ +This parser does not fail. -/ def take_until (p : char → bool) : parser_t m string := take_while (λ c, !p c) @@ -415,7 +415,7 @@ def lookahead (p : parser_t m α) : parser_t m α := | ok a s' := mk_eps_result a it | other := other -/-- `not_followed_by p` succeeds when parser_t m `p` fails -/ +/-- `not_followed_by p` succeeds when parser `p` fails -/ def not_followed_by (p : parser_t m α) (msg : string := "input") : parser_t m unit := λ it, do r ← p it, pure $ match r with