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

doc: include: currently applies to theorems only (#5206)

Browse source 
Fixes #5184
This commit is contained in:
Sebastian Ullrich 2024-08-30 14:51:50 +02:00 • committed by GitHub
parent 648239c6ec
commit e04a40ddc1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Parser/Command.lean
View file

@ -728,9 +728,10 @@ list, so it should be brief.
/--
`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all
declarations in the remainder of the current section, differing from the default behavior of
conditionally including variables based on use in the declaration header. `include` is usually
followed by the `in` combinator to limit the inclusion to the subsequent declaration.
theorems in the remainder of the current section, differing from the default behavior of
conditionally including variables based on use in the theorem header. Other commands are
not affected. `include` is usually followed by `in theorem ...` to limit the inclusion
to the subsequent declaration.
-/
@[builtin_command_parser] def «include» := leading_parser "include " >> many1 ident