chore: miscellaneous documentation typos (#10009)
This PR fixes several typos in documentation.
This commit is contained in:
thorimur
GitHub
parent
105879669e
commit
b2330fee2b
10 changed files with 67 additions and 56 deletions
|
|
@ -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`.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue