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

chore: make it clear how it is being parsed

Browse source 
We are planning to change the `<|>` precedence here.
This commit is contained in:
Leonardo de Moura 2021-09-16 13:41:01 -07:00
parent d65871241d
commit a823ebdbe0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Notation.lean
View file

@ -324,7 +324,7 @@ syntax config := atomic("(" &"config") " := " term ")"
syntax locationWildcard := "*"
syntax locationHyp := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
syntax locationTargets := (colGt ident)+ ("⊢" <|> "|-")?
syntax location := withPosition(" at " locationWildcard <|> locationHyp)
syntax location := withPosition(" at " (locationWildcard <|> locationHyp))
syntax (name := change) "change " term (location)? : tactic
syntax (name := changeWith) "change " term " with " term (location)? : tactic