From 9d14e4423ccaf50a32edd772884a2d033cfa0525 Mon Sep 17 00:00:00 2001 From: grunweg Date: Thu, 11 Jul 2024 00:03:11 +0200 Subject: [PATCH] chore: fix typo in doc-string (#4719) Fix a typo "to at" in a doc-string. --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 15a0beb37e..8b11a0fb2c 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -701,7 +701,7 @@ list, so it should be brief. @[builtin_command_parser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident -/-- No-op parser used as syntax kind for attaching remaining whitespace to at the end of the input. -/ +/-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/ @[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser "" builtin_initialize