Skip to content

Corrected link for custom operator priorities. #533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Corrected link for custom operator priorities. #533

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Manual/Classes/InstanceDecls.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,7 @@ instance instDecidableEqStringList : DecidableEq StringList
tag := "instance-priorities"
%%%

Instances may be assigned {deftech}_priorities_.
Instances may be assigned a {deftech}_priority_.
During instance synthesis, higher-priority instances are preferred; see {ref "instance-synth"}[the section on instance synthesis] for details of instance synthesis.

:::syntax prio open:=false (title := "Instance Priorities")
Expand Down
2 changes: 1 addition & 1 deletion Manual/IO/Threads.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ Tasks may be explicitly cancelled using {name}`IO.cancel`.
The Lean runtime maintains a thread pool for running tasks.
The size of the thread pool is determined by the environment variable {envVar (def := true)}`LEAN_NUM_THREADS` if it is set, or by the number of logical processors on the current machine otherwise.
The size of the thread pool is not a hard limit; in certain situations it may be exceeded to avoid deadlocks.
By default, these threads are used to run tasks; each task has a {deftech}_priority_ ({name}`Task.Priority`), and higher-priority tasks take precedence over lower-priority tasks.
By default, these threads are used to run tasks; each task has a {deftech}_task priority_ ({name}`Task.Priority`), and higher-priority tasks take precedence over lower-priority tasks.
Tasks may also be assigned to dedicated threads by spawning them with a sufficiently high priority.

{docstring Task (label := "type") (hideStructureConstructor := true) (hideFields := true)}
Expand Down