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

fix: space before 'at' in location

Browse source
This commit is contained in:
Daniel Selsam 2021-09-15 08:40:21 -07:00 • committed by Sebastian Ullrich
parent 6fb2a2b47b
commit 8d370f151f
3 changed files with 3 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 := ("(" &"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

1
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -484,6 +484,7 @@ def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
(fun _ => throwError "format: uncaught backtrack exception")
def formatTerm := format $ categoryParser.formatter `term
def formatTactic := format $ categoryParser.formatter `tactic
def formatCommand := format $ categoryParser.formatter `command
builtin_initialize registerTraceClass `PrettyPrinter.format;

1
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -534,6 +534,7 @@ def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :
(fun _ => throwError "parenthesize: uncaught backtrack exception")
def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
def parenthesizeTactic := parenthesize $ categoryParser.parenthesizer `tactic 0
def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0
builtin_initialize registerTraceClass `PrettyPrinter.parenthesize