From c0b76704a02477df4a99b4fa1a4702bbf609732e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Oct 2018 11:56:34 -0700 Subject: [PATCH] chore(library/init/lean/parser/level): typo --- library/init/lean/parser/level.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/level.lean b/library/init/lean/parser/level.lean index 52fde0abf5..7c3e0dfb39 100644 --- a/library/init/lean/parser/level.lean +++ b/library/init/lean/parser/level.lean @@ -16,7 +16,7 @@ open combinators parser.has_view monad_parsec def level_parser_m := rec_t nat syntax basic_parser_m abbreviation level_parser := level_parser_m syntax -/-- A term parser for a suffix or infix notation that accepts a preceding term. -/ +/-- A level parser for a suffix or infix notation that accepts a preceding term level. -/ @[derive monad alternative monad_reader monad_state monad_parsec monad_except monad_rec monad_basic_parser] def trailing_level_parser_m := reader_t syntax level_parser_m abbreviation trailing_level_parser := trailing_level_parser_m syntax