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

chore: fix typo in doc-string (#4719)

Browse source 
Fix a typo "to at" in a doc-string.
This commit is contained in:
grunweg 2024-07-11 00:03:11 +02:00 • committed by GitHub
parent 0c7859a7dd
commit 9d14e4423c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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/Lean/Parser/Command.lean
View file

@ -701,7 +701,7 @@ list, so it should be brief.
@[builtin_command_parser] def genInjectiveTheorems := leading_parser
"gen_injective_theorems% " >> ident
/-- No-op parser used as syntax kind for attaching remaining whitespace to at the end of the input. -/
/-- No-op parser used as syntax kind for attaching remaining whitespace at the end of the input. -/
@[run_builtin_parser_attribute_hooks] def eoi : Parser := leading_parser ""
builtin_initialize