From e2bcf179acc94a452002408179fa98978c228e8a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Jul 2019 10:33:51 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): missing `trim` --- library/init/lean/parser/parser.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 7fab5fb00c..e932a7a612 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -801,6 +801,8 @@ def unicodeSymbolInfo (sym asciiSym : String) (lbp : Option Nat) : ParserInfo := fun _ => unicodeSymbolFnAux sym asciiSym ("expected '" ++ sym ++ "' or '" ++ asciiSym ++ "'") @[inline] def unicodeSymbol {k : ParserKind} (sym asciiSym : String) (lbp : Option Nat := none) : Parser k := +let sym := sym.trim; +let asciiSym := asciiSym.trim; { info := unicodeSymbolInfo sym asciiSym lbp, fn := unicodeSymbolFn sym asciiSym }