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

chore: move helper functions to Parser.lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-14 13:33:20 -08:00
parent 15a2d7d8ca
commit dd2936d28e
2 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Lean/Parser/Parser.lean
View file

@ -1809,6 +1809,20 @@ mkAntiquot "fieldIdx" `fieldIdx <|>
{ fn := fun _ => fieldIdxFn,
info := mkAtomicInfo "fieldIdx" }
/- Helper functions for defining simple parsers -/
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser (lbp - 1)
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser lbp
end Parser
namespace Syntax

14
src/Init/Lean/Parser/Term.lean
View file

@ -9,20 +9,6 @@ import Init.Lean.Parser.Level
namespace Lean
namespace Parser
/- Helper functions for defining simple parsers -/
def unicodeInfixR (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser (lbp - 1)
def infixR (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser (lbp - 1)
def unicodeInfixL (sym : String) (asciiSym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> unicodeSymbol sym asciiSym lbp >> termParser lbp
def infixL (sym : String) (lbp : Nat) : TrailingParser :=
pushLeading >> symbol sym lbp >> termParser lbp
namespace Term
/- Built-in parsers -/