max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/parser/level): typo

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-12 11:56:34 -07:00
parent 15a25d5aa9
commit c0b76704a0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/level.lean
View file

@ -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