From b2330fee2b1f10be6d32e64dd25df185d7b76e1d Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Wed, 20 Aug 2025 17:39:03 -0400 Subject: [PATCH] chore: miscellaneous documentation typos (#10009) This PR fixes several typos in documentation. --- src/Init/Prelude.lean | 2 +- src/Lean/Elab/BuiltinTerm.lean | 2 +- src/Lean/Environment.lean | 4 +- src/Lean/ImportingFlag.lean | 2 +- src/Lean/Meta/InferType.lean | 69 +++++++++++++++++------------- src/Lean/Meta/Tactic/TryThis.lean | 8 ++-- src/Std/Sync/Channel.lean | 24 +++++------ src/lake/Lake/Build/Common.lean | 6 +-- src/lake/Lake/Build/Data.lean | 4 +- src/lake/Lake/Build/Job/Monad.lean | 2 +- 10 files changed, 67 insertions(+), 56 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1731302659..c64a61217f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3678,7 +3678,7 @@ class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where export MonadReader (read) /-- -Retrieves the local value whose type is `ρ`. This is useful when a monad supports reading more that +Retrieves the local value whose type is `ρ`. This is useful when a monad supports reading more than one type of value. Use `read` for a version that expects the type `ρ` to be inferred from `m`. diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 1e6e11cc4e..c85344c1f9 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -97,7 +97,7 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level := | none => if (← mvarId.isDelayedAssigned) then -- We can try to improve this case if needed. - throwError "synthetic hole has already beend defined and delayed assigned with an incompatible local context" + throwError "synthetic hole has already been defined and delayed-assigned with an incompatible local context" else if lctx.isSubPrefixOf mvarDecl.lctx then let mvarNew ← mkNewHole () mvarId.assign mvarNew diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index bdf720446a..d6f394afaf 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -804,7 +804,7 @@ declarations from `realizeConst`, which are not restricted to the current prefix which may escape the branch(es) they have been realized on such as when looking into the type `Expr` of a declaration found on another branch. Thus when we cannot find the declaration using the fast prefix-based lookup, we fall back to waiting for and looking at the realizations from all branches. -To avoid this expensive search for realizations from other branches, `skipRealize` can set to ensure +To avoid this expensive search for realizations from other branches, `skipRealize` can be set to ensure negative lookups are as fast as positive ones. Use `findTask` instead if any blocking should be avoided. @@ -1536,7 +1536,7 @@ An environment extension with support for storing/retrieving entries from a .ole - β is the type of values used to update the state. - σ is the actual state. -For most extensions, α and β coincide. `α` and ‵β` do not coincide for extensions where the data +For most extensions, α and β coincide. `α` and `β` do not coincide for extensions where the data used to update the state contains elements which cannot be stored in files (for example, closures). During elaboration of a module, state of type `σ` can be both read and written. When elaboration is diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean index df9b380487..6d91453d9a 100644 --- a/src/Lean/ImportingFlag.lean +++ b/src/Lean/ImportingFlag.lean @@ -43,7 +43,7 @@ def initializing : IO Bool := /-- Execute `x` with "importing" flag turned on. -When the "importing" flag is set to true, we allow user-extensions defined with with +When the "importing" flag is set to true, we allow user-extensions defined with the `initialize` command to update global references. IMPORTANT: There is no semaphore controlling the access to these global references. We assume these global references are updated by a single execution thread. diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 9fd4b96d0a..11fd5413ca 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -17,15 +17,16 @@ namespace Lean Auxiliary function for instantiating the loose bound variables in `e` with `args[start...stop]`. This function is similar to `instantiateRevRange`, but it applies beta-reduction when we instantiate a bound variable with a lambda expression. + Example: Given the term `#0 a`, and `start := 0, stop := 1, args := #[fun x => x]` the result is `a` instead of `(fun x => x) a`. This reduction is useful when we are inferring the type of eliminator-like applications. For example, given `(n m : Nat) (f : Nat → Nat) (h : m = n)`, the type of `Eq.subst (motive := fun x => f m = f x) h rfl` -is `motive n` which is `(fun (x : Nat) => f m = f x) n` -This function reduces the new application to `f m = f n` +is `motive n` which is `(fun (x : Nat) => f m = f x) n`. +This function reduces the new application to `f m = f n`. -We use it to implement `inferAppType` +We use this to implement `inferAppType`. -/ partial def Expr.instantiateBetaRevRange (e : Expr) (start : Nat) (stop : Nat) (args : Array Expr) : Expr := if e.hasLooseBVars && stop > start then @@ -187,7 +188,7 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do Ensure `MetaM` configuration is strong enough for inferring/checking types. For example, `beta := true` is essential when type checking. -Remark: we previously use the default configuration here, but this is problematic +Remark: we previously used the default configuration here, but this is problematic because it overrides unrelated configurations. -/ @[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := @@ -218,8 +219,10 @@ def inferTypeImp (e : Expr) : MetaM Expr := withIncRecDepth <| withInferTypeConfig (infer e) /-- - Return `LBool.true` if given level is always equivalent to universe level zero. - It is used to implement `isProp`. -/ +Return `LBool.true` if given level is always equivalent to universe level zero. + +This is used to implement `isProp`. +-/ private def isAlwaysZero : Level → Bool | .zero .. => true | .mvar .. => false @@ -230,8 +233,10 @@ private def isAlwaysZero : Level → Bool /-- `isArrowProp type n` is an "approximate" predicate which returns `LBool.true` - if `type` is of the form `A_1 -> ... -> A_n -> Prop`. - Remark: `type` can be a dependent arrow. -/ +if `type` is of the form `A_1 → ... → A_n → Prop`. + +Remark: `type` can be a dependent arrow. +-/ private partial def isArrowProp : Expr → Nat → MetaM LBool | .sort u, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool | .forallE .., 0 => return LBool.false @@ -241,8 +246,9 @@ private partial def isArrowProp : Expr → Nat → MetaM LBool | _, _ => return LBool.undef /-- - `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true` - if `f` applied to `n` arguments is a proposition. -/ +`isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true` +if `f` applied to `n` arguments is a proposition. +-/ private partial def isPropQuickApp : Expr → Nat → MetaM LBool | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProp constType arity | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType arity @@ -255,8 +261,9 @@ private partial def isPropQuickApp : Expr → Nat → MetaM LBool | _, _ => return LBool.undef /-- - `isPropQuick e` is an "approximate" predicate which returns `LBool.true` - if `e` is a proposition. -/ +`isPropQuick e` is an "approximate" predicate which returns `LBool.true` +if `e` is a proposition. +-/ partial def isPropQuick : Expr → MetaM LBool | .bvar .. => return LBool.undef | .lit .. => return LBool.false @@ -273,10 +280,10 @@ partial def isPropQuick : Expr → MetaM LBool /-- `isProp e` returns `true` if `e` is a proposition. -If `e` contains metavariables, it may not be possible -to decide whether is a proposition or not. We return `false` in this -case. We considered using `LBool` and retuning `LBool.undef`, but -we have no applications for it. + +If `e` contains metavariables, it may not be possible to decide whether it is a proposition or not. +We return `false` in this case. We considered using `LBool` and returning `LBool.undef`, but we +have no applications for it. -/ def isProp (e : Expr) : MetaM Bool := do match (← isPropQuick e) with @@ -360,16 +367,18 @@ where /-- `isArrowProposition type n` is an "approximate" predicate which returns `LBool.true` - if `type` is of the form `A_1 -> ... -> A_n -> B`, where `B` is a proposition. - Remark: `type` can be a dependent arrow. +if `type` is of the form `A_1 → ... → A_n → B`, where `B` is a proposition. + +Remark: `type` can be a dependent arrow. -/ private def isArrowProposition (e : Expr) (n : Nat) : MetaM LBool := return (← isArrowProposition' e n).toLBool mutual /-- -`isProofQuickApp f n` is an "approximate" predicate which returns `LBool.true` -if `f` applied to `n` arguments is a proof. -/ +`isProofQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to +`n` arguments is a proof. +-/ private partial def isProofQuickApp : Expr → Nat → MetaM LBool | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProposition constType arity | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType arity @@ -382,8 +391,8 @@ private partial def isProofQuickApp : Expr → Nat → MetaM LBool | _, _ => return LBool.undef /-- -`isProofQuick e` is an "approximate" predicate which returns `LBool.true` -if `e` is a proof. -/ +`isProofQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a proof. +-/ partial def isProofQuick : Expr → MetaM LBool | .bvar .. => return LBool.undef | .lit .. => return LBool.false @@ -407,9 +416,10 @@ def isProof (e : Expr) : MetaM Bool := do | .undef => Meta.isProp (← inferType e) /-- - `isArrowType type n` is an "approximate" predicate which returns `LBool.true` - if `type` is of the form `A_1 -> ... -> A_n -> Sort _`. - Remark: `type` can be a dependent arrow. -/ +`isArrowType type n` is an "approximate" predicate which returns `LBool.true` if `type` is of the +form `A_1 → ... → A_n → Sort _`. + +Remark: `type` can be a dependent arrow. -/ private partial def isArrowType : Expr → Nat → MetaM LBool | .sort .., 0 => return LBool.true | .forallE .., 0 => return LBool.false @@ -419,8 +429,9 @@ private partial def isArrowType : Expr → Nat → MetaM LBool | _, _ => return LBool.undef /-- -`isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true` - if `f` applied to `n` arguments is a type. -/ +`isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to +`n` arguments is a type. +-/ private partial def isTypeQuickApp : Expr → Nat → MetaM LBool | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowType constType arity | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowType fvarType arity @@ -433,8 +444,8 @@ private partial def isTypeQuickApp : Expr → Nat → MetaM LBool | _, _ => return LBool.undef /-- -`isTypeQuick e` is an "approximate" predicate which returns `LBool.true` -if `e` is a type. -/ +`isTypeQuick e` is an "approximate" predicate which returns `LBool.true` if `e` is a type. +-/ partial def isTypeQuick : Expr → MetaM LBool | .bvar .. => return LBool.undef | .lit .. => return LBool.false diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean index a3ed73a881..d7ed078429 100644 --- a/src/Lean/Meta/Tactic/TryThis.lean +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -163,8 +163,8 @@ private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion) The parameters are: * `ref`: the span of the info diagnostic * `s`: a `Suggestion`, which contains - * `suggestion`: the replacement text; - * `preInfo?`: an optional string shown immediately after the replacement text in the widget + * `suggestion`: the replacement text + * `preInfo?`: an optional string shown immediately before the replacement text in the widget message (only) * `postInfo?`: an optional string shown immediately after the replacement text in the widget message (only) @@ -198,8 +198,8 @@ def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := The parameters are: * `ref`: the span of the info diagnostic * `suggestions`: an array of `Suggestion`s, which each contain - * `suggestion`: the replacement text; - * `preInfo?`: an optional string shown immediately after the replacement text in the widget + * `suggestion`: the replacement text + * `preInfo?`: an optional string shown immediately before the replacement text in the widget message (only) * `postInfo?`: an optional string shown immediately after the replacement text in the widget message (only) diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean index a5e66bc5ab..bad33f0355 100644 --- a/src/Std/Sync/Channel.lean +++ b/src/Std/Sync/Channel.lean @@ -19,7 +19,7 @@ multi-consumer FIFO channel that offers both bounded and unbounded buffering as and asynchronous APIs. Additionally `Std.CloseableChannel` is provided in case closing the channel is of interest. -The two are distinct as the non closable `Std.Channel` can never throw errors which makes +The two are distinct as the non-closeable `Std.Channel` can never throw errors which makes for cleaner code. -/ @@ -67,7 +67,7 @@ private def Consumer.resolve (c : Consumer α) (x : Option α) : BaseIO Bool := waiter.race lose win /-- -The central state structure for an unbounded channel, maintains the following invariants: +The central state structure for an unbounded channel. Maintains the following invariants: 1. `values = ∅ ∨ consumers = ∅` 2. `closed = true → consumers = ∅` -/ @@ -205,7 +205,7 @@ private def recvSelector (ch : Unbounded α) : Selector (Option α) where end Unbounded /-- -The central state structure for a zero buffer channel, maintains the following invariants: +The central state structure for a zero buffer channel. Maintains the following invariants: 1. `producers = ∅ ∨ consumers = ∅` 2. `closed = true → consumers = ∅` -/ @@ -363,7 +363,7 @@ private def Bounded.Consumer.resolve (c : Bounded.Consumer α) (b : Bool) : Base c.promise.resolve b /-- -The central state structure for a bounded channel, maintains the following invariants: +The central state structure for a bounded channel. Maintains the following invariants: 1. `0 < capacity` 2. `0 < bufCount → consumers = ∅` 3. `bufCount < capacity → producers = ∅` @@ -393,15 +393,15 @@ private structure Bounded.State (α : Type) where -/ capacity : Nat /-- - The buffer space for the channel, slots with `some v` contain a value that is waiting for - consumption, the slots with `none` are free for enqueueing. + The buffer space for the channel. Slots with `some v` contain a value that is waiting for + consumption; the slots with `none` are free for enqueueing. Note that this is a `Vector` of `IO.Ref (Option α)` as the `buf` itself is shared across threads and would thus keep getting copied if it was a `Vector (Option α)` instead. -/ buf : Vector (IO.Ref (Option α)) capacity /-- - How many slots in `buf` are currently used, this is used to disambiguate between an empty and a + How many slots in `buf` are currently used. This is used to disambiguate between an empty and a full buffer without sacrificing a slot for indicating that. -/ bufCount : Nat @@ -651,7 +651,7 @@ instance : Nonempty (CloseableChannel.Sync α) := namespace CloseableChannel /-- -Create a new channel, if: +Create a new channel. If: - `capacity` is `none` it will be unbounded (the default) - `capacity` is `some 0` it will always force a rendezvous between sender and receiver - `capacity` is `some n` with `n > 0` it will use a buffer of size `n` and begin blocking once it @@ -664,8 +664,8 @@ def new (capacity : Option Nat := none) : BaseIO (CloseableChannel α) := do | some (n + 1) => return .bounded (← CloseableChannel.Bounded.new (n + 1) (by omega)) /-- -Try to send a value to the channel, if this can be completed right away without blocking return -`true`, otherwise don't send the value and return `false`. +Try to send a value to the channel. If this can be completed right away without blocking return +`true`; otherwise, don't send the value and return `false`. -/ def trySend (ch : CloseableChannel α) (v : α) : BaseIO Bool := match ch with @@ -808,7 +808,7 @@ end CloseableChannel /-- A multi-producer multi-consumer FIFO channel that offers both bounded and unbounded buffering -and an asynchronous API, to switch into synchronous mode use `Channel.sync`. +and an asynchronous API. To switch into synchronous mode use `Channel.sync`. If a channel needs to be closed to indicate some sort of completion event use `Std.CloseableChannel` instead. Note that `Std.CloseableChannel` introduces a need for error handling in some cases, thus @@ -866,7 +866,7 @@ def recv [Inhabited α] (ch : Channel α) : BaseIO (Task α) := do open Internal.IO.Async in /-- -Creates a `Selector` that resolves once `ch` has data available and provides that that data. +Creates a `Selector` that resolves once `ch` has data available and provides that data. -/ def recvSelector [Inhabited α] (ch : Channel α) : Selector α := let sel := CloseableChannel.recvSelector ch.inner diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index f03546762b..32aa735c72 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -539,7 +539,7 @@ If `text := true`, `file` is handled as a text file rather than a binary file. /-! ## Common Builds -/ /-- -A build job for binary file that is expected to already exist (e.g., a data blob). +A build job for a binary file that is expected to already exist (e.g., a data blob). Any byte difference in a binary file will trigger a rebuild of its dependents. -/ @@ -548,7 +548,7 @@ def inputBinFile (path : FilePath) : SpawnM (Job FilePath) := Job.async do return path /-- -A build job for text file that is expected to already exist (e.g., a source file). +A build job for a text file that is expected to already exist (e.g., a source file). Text file traces have normalized line endings to avoid unnecessary rebuilds across platforms. -/ @@ -557,7 +557,7 @@ def inputTextFile (path : FilePath) : SpawnM (Job FilePath) := Job.async do return path /-- -A build job for file that is expected to already exist (e.g., a data blob or source file). +A build job for a file that is expected to already exist (e.g., a data blob or source file). If `text := true`, the file is handled as a text file rather than a binary file. Any byte difference in a binary file will trigger a rebuild of its dependents. diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean index 530e1f8c07..24d823ab80 100644 --- a/src/lake/Lake/Build/Data.lean +++ b/src/lake/Lake/Build/Data.lean @@ -128,7 +128,7 @@ as needed (via `custom_data`). opaque CustomOut (target : Name × Name) : Type /-- -The open type family which maps a custom package targetto its output type. +The open type family which maps a custom package target to its output type. It is an open type, meaning additional mappings can be add lazily as needed (via `custom_data`). @@ -174,7 +174,7 @@ instance [FamilyOut DataType Package.facetKind α] open Parser Command -/-- Macro for declaring new `DatayType`. -/ +/-- Macro for declaring a new `DataType`. -/ scoped macro (name := dataTypeDecl) doc?:optional(docComment) "data_type " kind:ident " : " ty:term : command => do diff --git a/src/lake/Lake/Build/Job/Monad.lean b/src/lake/Lake/Build/Job/Monad.lean index 52992578cf..c20309d471 100644 --- a/src/lake/Lake/Build/Job/Monad.lean +++ b/src/lake/Lake/Build/Job/Monad.lean @@ -135,7 +135,7 @@ namespace Job : SpawnM (Job α) := fun fetch pkg? stack store ctx => .ofTask (caption := caption) <$> do BaseIO.asTask (prio := prio) do (withLoggedIO act) fetch pkg? stack store ctx {} -/-- Wait a the job to complete and return the result. -/ +/-- Wait for a job to complete and return the result. -/ @[inline] protected def wait (self : Job α) : BaseIO (JobResult α) := do IO.wait self.task