Skip to content

Commit 52892d3

Browse files
authored
chore: add tag to header "Section Variables" (#264)
1 parent 9ec7d8c commit 52892d3

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

Manual/Language.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -418,6 +418,9 @@ unknown identifier 'cupcake'
418418
:::
419419

420420
### Section Variables
421+
%%%
422+
tag := "section-variables"
423+
%%%
421424

422425
{deftech}_Section variables_ are parameters that are automatically added to declarations that mention them.
423426
This occurs whether or not the option {option}`autoImplicit` is {lean}`true`.

0 commit comments

Comments
 (0)