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 }