diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index 366d29b6ecc5..b7ad27bd2958 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -102,7 +102,7 @@ noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h ⟨xp.val, fun _ => xp.property⟩) (fun hp => ⟨choice h, fun h => absurd h hp⟩) -/-- the Hilbert epsilon Function -/ +/-- The Hilbert epsilon function. -/ noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α := (strongIndefiniteDescription p h).val diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index 7221eb929f28..c8576cec3746 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -144,7 +144,7 @@ instance : ToBool Bool where Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns it and ignores `y`; otherwise, runs `y` and returns its result. -This a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>` +This is a monadic counterpart to the short-circuiting `||` operator, usually accessed via the `<||>` operator. -/ @[macro_inline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do @@ -161,7 +161,7 @@ recommended_spelling "orM" for "<||>" in [orM, «term_<||>_»] Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise, returns the original result of `x`. -This a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>` +This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>` operator. -/ @[macro_inline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do diff --git a/src/Init/Core.lean b/src/Init/Core.lean index a08aef2cb415..5789c80a0633 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -337,7 +337,7 @@ inductive Exists {α : Sort u} (p : α → Prop) : Prop where An indication of whether a loop's body terminated early that's used to compile the `for x in xs` notation. -A collection's `ForIn` or `ForIn'` instance describe's how to iterate over its elements. The monadic +A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state used to implement features such as `let mut`. -/ @@ -510,12 +510,12 @@ abbrev SSuperset [HasSSubset α] (a b : α) := SSubset b a /-- Notation type class for the union operation `∪`. -/ class Union (α : Type u) where - /-- `a ∪ b` is the union of`a` and `b`. -/ + /-- `a ∪ b` is the union of `a` and `b`. -/ union : α → α → α /-- Notation type class for the intersection operation `∩`. -/ class Inter (α : Type u) where - /-- `a ∩ b` is the intersection of`a` and `b`. -/ + /-- `a ∩ b` is the intersection of `a` and `b`. -/ inter : α → α → α /-- Notation type class for the set difference `\`. -/ @@ -538,10 +538,10 @@ infix:50 " ⊇ " => Superset /-- Strict superset relation: `a ⊃ b` -/ infix:50 " ⊃ " => SSuperset -/-- `a ∪ b` is the union of`a` and `b`. -/ +/-- `a ∪ b` is the union of `a` and `b`. -/ infixl:65 " ∪ " => Union.union -/-- `a ∩ b` is the intersection of`a` and `b`. -/ +/-- `a ∩ b` is the intersection of `a` and `b`. -/ infixl:70 " ∩ " => Inter.inter /-- diff --git a/src/Init/Data/Iterators/PostconditionMonad.lean b/src/Init/Data/Iterators/PostconditionMonad.lean index 4e1dc9f02f2f..205bcbc8ffe4 100644 --- a/src/Init/Data/Iterators/PostconditionMonad.lean +++ b/src/Init/Data/Iterators/PostconditionMonad.lean @@ -72,7 +72,7 @@ def PostconditionT.liftWithProperty {α : Type w} {m : Type w → Type w'} {P : ⟨P, x⟩ /-- -Given a function `f : α → β`, returns a a function `PostconditionT m α → PostconditionT m β`, +Given a function `f : α → β`, returns a function `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a functor. The postcondition of the `x.map f` states that the return value is the image under `f` of some @@ -85,7 +85,7 @@ protected def PostconditionT.map {m : Type w → Type w'} [Functor m] {α : Type (fun a => ⟨f a.val, _, rfl⟩) <$> x.operation⟩ /-- -Given a function `α → PostconditionT m β`, returns a a function +Given a function `α → PostconditionT m β`, returns a function `PostconditionT m α → PostconditionT m β`, turning `PostconditionT m` into a monad. -/ @[always_inline, inline, expose] diff --git a/src/Init/Data/LawfulHashable.lean b/src/Init/Data/LawfulHashable.lean index 5c054351e03d..ad09888fc660 100644 --- a/src/Init/Data/LawfulHashable.lean +++ b/src/Init/Data/LawfulHashable.lean @@ -11,7 +11,7 @@ public import Init.Core public section /-- -The `BEq α` and `Hashable α` instances on `α` are compatible. This means that that `a == b` implies +The `BEq α` and `Hashable α` instances on `α` are compatible. This means that `a == b` implies `hash a = hash b`. This is automatic if the `BEq` instance is lawful. diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index 95ea6dbe2b59..0d35b80b42db 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -50,7 +50,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead. Applies the monadic action `f` to every element in the list, left-to-right, and returns the list of results. -This implementation is tail recursive. `List.mapM'` is a a non-tail-recursive variant that may be +This implementation is tail recursive. `List.mapM'` is a non-tail-recursive variant that may be more convenient to reason about. `List.forM` is the variant that discards the results and `List.mapA` is the variant that works with `Applicative`. -/ @@ -107,7 +107,7 @@ Applies the monadic action `f` to the corresponding elements of two lists, left- at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)` for lawful `Monad` instances. -This implementation is tail recursive. `List.zipWithM'` is a a non-tail-recursive variant that may +This implementation is tail recursive. `List.zipWithM'` is a non-tail-recursive variant that may be more convenient to reason about. -/ @[inline, expose] diff --git a/src/Init/Data/Order/Ord.lean b/src/Init/Data/Order/Ord.lean index 2cfba68796c5..0d06611ee828 100644 --- a/src/Init/Data/Order/Ord.lean +++ b/src/Init/Data/Order/Ord.lean @@ -46,7 +46,7 @@ theorem ne_of_cmp_ne_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCm end ReflCmp -/-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/ +/-- A typeclass for ordered types for which `compare a a = .eq` for all `a`. -/ abbrev ReflOrd (α : Type u) [Ord α] := ReflCmp (compare : α → α → Ordering) @[simp] diff --git a/src/Init/Data/Slice/Notation.lean b/src/Init/Data/Slice/Notation.lean index 30147faa991a..5a35563d5c32 100644 --- a/src/Init/Data/Slice/Notation.lean +++ b/src/Init/Data/Slice/Notation.lean @@ -40,7 +40,7 @@ class Rcc.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type This typeclass indicates how to obtain slices of elements of {lit}`α` over ranges in the index type {lit}`β`, the ranges being left-closed right-open. -The type of resulting the slices is {lit}`γ`. +The type of the resulting slices is {lit}`γ`. -/ class Rco.Sliceable (α : Type u) (β : outParam (Type v)) (γ : outParam (Type w)) where /-- diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean index 6e0495122471..720e1bcd3d01 100644 --- a/src/Init/Data/String/Pattern/String.lean +++ b/src/Init/Data/String/Pattern/String.lean @@ -119,7 +119,7 @@ instance (s : Slice) : Std.Iterator (ForwardSliceSearcher s) Id (SearchStep s) w -- **Invariant 1:** we have already covered everything up until `stackPos - needlePos` (exclusive), -- with matches and rejections. -- **Invariant 2:** `stackPos - needlePos` is a valid position - -- **Invariant 3:** the range from from `stackPos - needlePos` to `stackPos` (exclusive) is a + -- **Invariant 3:** the range from `stackPos - needlePos` to `stackPos` (exclusive) is a -- prefix of the pattern. if h₁ : stackPos < s.rawEndPos then let stackByte := s.getUTF8Byte stackPos h₁ diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean index 3d3eba1fdd47..e04bbd69568a 100644 --- a/src/Init/Data/String/Slice.lean +++ b/src/Init/Data/String/Slice.lean @@ -20,7 +20,7 @@ functionality for searching for various kinds of pattern matches in slices to it provide subslices according to matches etc. The key design principles behind this module are: - Instead of providing one function per kind of pattern the API is generic over various kinds of patterns. Thus it only provides e.g. one kind of function for looking for the position of the - first occurence of a pattern. Currently the supported patterns are: + first occurrence of a pattern. Currently the supported patterns are: - {name}`Char` - {lean}`Char → Bool` - {name}`String` and {name}`String.Slice` (partially: doing non trivial searches backwards is not diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 1b5126a68aaf..8acb2f0da7ec 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -523,7 +523,7 @@ macro_rules | `(bif $c then $t else $e) => `(cond $c $t $e) /-- -Haskell-like pipe operator `<|`. `f <| x` means the same as the same as `f x`, +Haskell-like pipe operator `<|`. `f <| x` means the same as `f x`, except that it parses `x` with lower precedence, which means that `f <| g <| x` is interpreted as `f (g x)` rather than `(f g) x`. -/ @@ -557,7 +557,7 @@ macro_rules | `($a |> $f) => `($f $a) /-- -Alternative syntax for `<|`. `f $ x` means the same as the same as `f x`, +Alternative syntax for `<|`. `f $ x` means the same as `f x`, except that it parses `x` with lower precedence, which means that `f $ g $ x` is interpreted as `f (g x)` rather than `(f g) x`. -/ diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 995d8e3dd502..833a94fdaa28 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -120,7 +120,7 @@ calc _ = z := pyz ``` It is also possible to write the *first* relation as `\n _ = := -`. This is useful for aligning relation symbols, especially on longer: +`. This is useful for aligning relation symbols, especially on longer identifiers: ``` calc abc diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 01dd7a449416..e177fd10a8f2 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -907,7 +907,7 @@ instance [Inhabited α] : Inhabited (ULift α) where Lifts a type or proposition to a higher universe level. `PULift α` wraps a value of type `α`. It is a generalization of -`PLift` that allows lifting values who's type may live in `Sort s`. +`PLift` that allows lifting values whose type may live in `Sort s`. It also subsumes `PLift`. -/ -- The universe variable `r` is written first so that `ULift.{r} α` can be used @@ -3525,7 +3525,7 @@ instance : DecidableEq String.Pos.Raw := /-- A region or slice of some underlying string. -A substring contains an string together with the start and end byte positions of a region of +A substring contains a string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many substrings of the same underlying string may exist with very little overhead, and they are more convenient than tracking the bounds by hand. diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 68b2998a3770..5a3764d94692 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -150,7 +150,7 @@ def parent (p : FilePath) : Option FilePath := /-- Extracts the last element of a path if it is a file or directory name. -Returns `none ` if the last entry is a special name (such as `.` or `..`) or if the path is the root +Returns `none` if the last entry is a special name (such as `.` or `..`) or if the path is the root directory. -/ def fileName (p : FilePath) : Option String := diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 33c12f676ec8..8afa85954299 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -561,7 +561,7 @@ Waits for the task to finish, then returns its result. return t.get /-- -Waits until any of the tasks in the list has finished, then return its result. +Waits until any of the tasks in the list has finished, then returns its result. -/ @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α)) (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α := @@ -679,7 +679,7 @@ File handles wrap the underlying operating system's file descriptors. There is n to close a file: when the last reference to a file handle is dropped, the file is closed automatically. -Handles have an associated read/write cursor that determines the where reads and writes occur in the +Handles have an associated read/write cursor that determines where reads and writes occur in the file. -/ opaque FS.Handle : Type := Unit @@ -790,7 +790,7 @@ An exception is thrown if the file cannot be opened. /-- Acquires an exclusive or shared lock on the handle. Blocks to wait for the lock if necessary. -Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it +Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it works on Unix-like systems but not on Windows. -/ @[extern "lean_io_prim_handle_lock"] opaque lock (h : @& Handle) (exclusive := true) : IO Unit @@ -798,7 +798,7 @@ works on Unix-like systems but not on Windows. Tries to acquire an exclusive or shared lock on the handle and returns `true` if successful. Will not block if the lock cannot be acquired, but instead returns `false`. -Acquiring a exclusive lock while already possessing a shared lock will **not** reliably succeed: it +Acquiring an exclusive lock while already possessing a shared lock will **not** reliably succeed: it works on Unix-like systems but not on Windows. -/ @[extern "lean_io_prim_handle_try_lock"] opaque tryLock (h : @& Handle) (exclusive := true) : IO Bool @@ -1350,7 +1350,7 @@ def withTempFile [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : Handle → Fi removeFile path /-- -Creates a temporary directory in the most secure manner possible, providing a its path to an `IO` +Creates a temporary directory in the most secure manner possible, providing its path to an `IO` action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how or when they were created. @@ -1480,7 +1480,7 @@ possible to close the child's standard input before the process terminates, whic @[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig) /-- -Blocks until the child process has exited and return its exit code. +Blocks until the child process has exited and returns its exit code. -/ @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32 @@ -1586,7 +1586,7 @@ end Process /-- POSIX-style file permissions. -The `FileRight` structure describes these permissions for a file's owner, members of it's designated +The `FileRight` structure describes these permissions for a file's owner, members of its designated group, and all others. -/ structure AccessRight where @@ -1863,7 +1863,7 @@ unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a set_option linter.unusedVariables false in /-- -Discards the passed owned reference. This leads to `a` any any object reachable from it never being +Discards the passed owned reference. This leads to `a` and any object reachable from it never being freed. This can be a useful optimization for eliding deallocation time of big object graphs that are kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent` would be similarly costly to deallocation). It is still considered a safe operation as it cannot diff --git a/src/Init/WF.lean b/src/Init/WF.lean index fd167d21cc8c..8dbc7d32fd54 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -463,7 +463,7 @@ variable {motive : α → Sort v} variable (h : α → Nat) variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x) -/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/ +/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates to a ground term. -/ def Nat.eager (n : Nat) : Nat := if Nat.beq n n = true then n else n @@ -474,8 +474,8 @@ A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a its higher order function argument `F` to invoke its argument only on values `y` that are smaller than `x` with regard to `h`. -In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely: -when `h x` evalutes to a ground value) +In contrast to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely: +when `h x` evaluates to a ground value) -/ def Nat.fix : (x : α) → motive x := diff --git a/src/Std/Data/ExtHashMap/Basic.lean b/src/Std/Data/ExtHashMap/Basic.lean index 9316f13e58f1..0295cf8fd711 100644 --- a/src/Std/Data/ExtHashMap/Basic.lean +++ b/src/Std/Data/ExtHashMap/Basic.lean @@ -107,7 +107,7 @@ def containsThenInsertIfNew [EquivBEq α] [LawfulHashable α] ⟨replaced, ⟨r⟩⟩ /-- -Checks whether a key is present in a map, returning the associate value, and inserts a value for +Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found. If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index ab1d167bc395..ff391137baec 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -108,7 +108,7 @@ instance : LawfulSingleton (α × β) (HashMap α β) := ⟨fun _ => rfl⟩ ⟨replaced, ⟨r⟩⟩ /-- -Checks whether a key is present in a map, returning the associate value, and inserts a value for +Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found. If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean index 96662bf7e2a6..a789a40c91c5 100644 --- a/src/Std/Do/SPred/DerivedLaws.lean +++ b/src/Std/Do/SPred/DerivedLaws.lean @@ -220,7 +220,7 @@ Decomposing assertions in postconditions into conjunctions of simpler predicates chance that automation will be able to prove the entailment of the postcondition and the next precondition. -/ class IsAnd (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where - /-- A proof the the decomposition is logically equivalent to the original predicate. -/ + /-- A proof that the decomposition is logically equivalent to the original predicate. -/ to_and : P ⊣⊢ₛ Q₁ ∧ Q₂ instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := pure_and.symm diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index 0734c92a6c4b..009e4d45d6b8 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -22,13 +22,13 @@ namespace Async This module provides a layered approach to asynchronous programming, combining monadic types, type classes, and concrete task types that work together in a cohesive system. -- **Monadic Types**: These types provide a good way to to chain and manipulate context. These +- **Monadic Types**: These types provide a good way to chain and manipulate context. These can contain a `Task`, enabling manipulation of both asynchronous and synchronous code. - **Concrete Task Types**: Concrete units of work that can be executed within these contexts. ## Monadic Types -These types provide a good way to to chain and manipulate context. These can contain a `Task`, +These types provide a good way to chain and manipulate context. These can contain a `Task`, enabling manipulation of both asynchronous and synchronous code. - `BaseAsync`: A monadic type for infallible asynchronous computations @@ -548,7 +548,7 @@ def concurrentlyAll (xs : Array (BaseAsync α)) (prio := Task.Priority.default) /-- Runs all computations concurrently and returns the result of the first one to finish. -All other results are lost, and the tasks are not cancelled, so they'll continue their executing +All other results are lost, and the tasks are not cancelled, so they'll continue their execution until the end. -/ @[inline, specialize] @@ -829,7 +829,7 @@ def concurrentlyAll (xs : Array (EAsync ε α)) (prio := Task.Priority.default) /-- Runs all computations concurrently and returns the result of the first one to finish. -All other results are lost, and the tasks are not cancelled, so they'll continue their executing +All other results are lost, and the tasks are not cancelled, so they'll continue their execution until the end. -/ @[inline, specialize] @@ -969,7 +969,7 @@ def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : As /-- Runs all computations concurrently and returns the result of the first one to finish. -All other results are lost, and the tasks are not cancelled, so they'll continue their executing +All other results are lost, and the tasks are not cancelled, so they'll continue their execution until the end. -/ @[inline, specialize] diff --git a/src/Std/Sync/Broadcast.lean b/src/Std/Sync/Broadcast.lean index 1b363f433cc5..03129cde64cd 100644 --- a/src/Std/Sync/Broadcast.lean +++ b/src/Std/Sync/Broadcast.lean @@ -540,7 +540,7 @@ def recv [Inhabited α] (ch : Broadcast.Receiver α) : BaseIO (Task (Option α)) open Internal.IO.Async in /-- -Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that that data. +Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data. -/ @[inline] def recvSelector [Inhabited α] (ch : Broadcast.Receiver α) : Selector (Option α) := diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean index a6fd56371fe5..644794e7b3eb 100644 --- a/src/Std/Sync/Channel.lean +++ b/src/Std/Sync/Channel.lean @@ -734,7 +734,7 @@ def recv (ch : CloseableChannel α) : BaseIO (Task (Option α)) := 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. In particular if `ch` is closed while waiting on this `Selector` and no data is available already this will resolve to `none`. -/ diff --git a/src/Std/Sync/Notify.lean b/src/Std/Sync/Notify.lean index f10051cbcdac..47563e37b9aa 100644 --- a/src/Std/Sync/Notify.lean +++ b/src/Std/Sync/Notify.lean @@ -43,7 +43,7 @@ def Notify.Consumer.resolve (c : Consumer α) (x : α) : BaseIO Bool := do waiter.race lose win /-- -The central state structure for an a `Notify`. +The central state structure for a `Notify`. -/ structure Notify.State where diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean index 1a71c78b9205..590db83ecad3 100644 --- a/src/Std/Tactic/BVDecide/Syntax.lean +++ b/src/Std/Tactic/BVDecide/Syntax.lean @@ -83,7 +83,7 @@ structure BVDecideConfig where -/ maxSteps : Nat := Lean.Meta.Simp.defaultMaxSteps /-- - Short-circuit multiplication as a abstraction-style optimization that triggers + Short-circuit multiplication as an abstraction-style optimization that triggers if matching multiplications are not needed to proof a goal. -/ shortCircuit : Bool := false diff --git a/src/Std/Time.lean b/src/Std/Time.lean index bd73a0c29f87..e8b32b8963b8 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -74,7 +74,7 @@ like `23:59:60` that is valid in ISO 8601. - `Minute.Ordinal`: Ranges from 0 to 59. - `Nanosecond.Ordinal`: Ranges from 0 to 999,999,999. - `Second.Ordinal`: Ranges from 0 to 60. - - `Weekday`: That is a inductive type with all the seven days. + - `Weekday`: That is an inductive type with all the seven days. ## Span