From 7fdfdb1784df4b42701dc3b6ccdcd404fa5a14f9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 6 Nov 2018 21:45:08 +0100 Subject: [PATCH] chore(library/init/lean/parser): remove unnecessary class constraints --- library/init/lean/parser/pratt.lean | 2 +- library/init/lean/parser/token.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/pratt.lean b/library/init/lean/parser/pratt.lean index 59604dd96f..1148aaa6e3 100644 --- a/library/init/lean/parser/pratt.lean +++ b/library/init/lean/parser/pratt.lean @@ -12,7 +12,7 @@ namespace lean.parser open monad_parsec combinators variables {base_m : Type → Type} -variables [monad base_m] [monad_basic_parser base_m] [monad_state parser_state base_m] [monad_parsec syntax base_m] [monad_reader parser_config base_m] +variables [monad base_m] [monad_basic_parser base_m] [monad_parsec syntax base_m] [monad_reader parser_config base_m] local notation `m` := rec_t nat syntax base_m local notation `parser` := m syntax diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 3094fcb8c8..f402074370 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -68,7 +68,7 @@ do start ← left_over, stop ← left_over, pure ⟨start, stop⟩ -variables [monad_state parser_state m] [monad_basic_parser m] +variables [monad_basic_parser m] private mutual def update_trailing, update_trailing_lst with update_trailing : substring → syntax → syntax