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

chore: "upgrate" to doc string

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-12 18:30:08 -07:00
parent 4af94b2f6d
commit 71229f45fb
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

@ -320,7 +320,7 @@ macro "admit" : tactic => `(exact sorry)
macro "sorry" : tactic => `(exact sorry)
macro "inferInstance" : tactic => `(exact inferInstance)
/- Optional configuration option for tactics -/
/-- Optional configuration option for tactics -/
syntax config := ("(" &"config" " := " term ")")
syntax locationWildcard := "*"