max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/parser/parser): missing trim

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-08 10:33:51 -07:00
parent 8b3d932212
commit e2bcf179ac
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/parser.lean
View file

@ -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 }