From e9b8e54dcc55c467a7ca42e57e0422695b88fc82 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 8 Mar 2022 18:54:05 +0100 Subject: [PATCH] feat: `scientific` parser alias for `scientificLit` --- src/Lean/Parser.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 6d8121c504..b0434f4398 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -26,6 +26,7 @@ builtin_initialize register_parser_alias "str" strLit register_parser_alias "char" charLit register_parser_alias "name" nameLit + register_parser_alias "scientific" scientificLit register_parser_alias ident register_parser_alias "colGt" checkColGt register_parser_alias "colGe" checkColGe