diff --git a/Manual/Classes/InstanceDecls.lean b/Manual/Classes/InstanceDecls.lean index 20f31659..778b66ab 100644 --- a/Manual/Classes/InstanceDecls.lean +++ b/Manual/Classes/InstanceDecls.lean @@ -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") diff --git a/Manual/IO/Threads.lean b/Manual/IO/Threads.lean index e420fc49..0d9204fb 100644 --- a/Manual/IO/Threads.lean +++ b/Manual/IO/Threads.lean @@ -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)}