From fa2d28e2da0fc03e95b644a3da89d41e3a9cc3ea Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 28 Mar 2025 23:30:53 +0100 Subject: [PATCH] doc: docstring details (#7711) This PR adds the last few missing docstrings that appear in the manual. --- src/Init/Control/EState.lean | 12 ++++++++++-- src/Init/Conv.lean | 4 ++++ src/Init/Data/String/Basic.lean | 12 ++++++++++-- src/Init/Data/ToString/Basic.lean | 7 +++++++ src/Init/Dynamic.lean | 12 +++++++++--- src/Init/Internal/Order/Basic.lean | 13 +++++++++++-- src/Init/Meta.lean | 6 ++++++ src/Init/MetaTypes.lean | 12 ++++++++---- src/Init/System/FilePath.lean | 1 + src/Init/System/IO.lean | 3 +++ src/Init/Util.lean | 22 +++++++++++++++++++++- src/lake/Lake/Config/LeanConfig.lean | 4 +++- 12 files changed, 93 insertions(+), 15 deletions(-) diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean index 030f10b142..db3edd97b2 100644 --- a/src/Init/Control/EState.lean +++ b/src/Init/Control/EState.lean @@ -29,8 +29,11 @@ namespace EStateM variable {ε σ α β : Type u} -/-- Alternative orElse operator that allows to select which exception should be used. - The default is to use the first exception since the standard `orElse` uses the second. -/ +/-- +Alternative orElse operator that allows callers to select which exception should be used when both +operations fail. The default is to use the first exception since the standard `orElse` uses the +second. +-/ @[always_inline, inline] protected def orElse' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s => let d := Backtrackable.save s; @@ -54,6 +57,11 @@ instance : MonadFinally (EStateM ε σ) := { | Result.error e₂ s => Result.error e₂ s } +/-- +Converts a state monad action into a state monad action with exceptions. + +The resulting action does not throw an exception. +-/ @[always_inline, inline] def fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α := fun s => match x.run s with | (a, s') => EStateM.Result.ok a s' diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 4bd2f9c3e0..1b38f36123 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -306,6 +306,10 @@ syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " convSe /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/ macro "try " t:convSeq : conv => `(conv| first | $t | skip) +/-- +`tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals +produced by `tac'`. +-/ macro:1 x:conv tk:" <;> " y:conv:0 : conv => `(conv| tactic' => (conv' => $x:conv) <;>%$tk (conv' => $y:conv)) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 4401e77364..ac8a690020 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1508,12 +1508,20 @@ Checks whether the substring can be interpreted as the decimal representation of A substring can be interpreted as a decimal natural number if it is not empty and all the characters in it are digits. -Use `Substring.toNat?` to convert such a string to a natural number. - +Use `Substring.toNat?` to convert such a substring to a natural number. -/ @[inline] def isNat (s : Substring) : Bool := s.all fun c => c.isDigit +/-- +Checks whether the substring can be interpreted as the decimal representation of a natural number, +returning the number if it can. + +A substring can be interpreted as a decimal natural number if it is not empty and all the characters +in it are digits. + +Use `Substring.isNat` to check whether the substring is such a substring. +-/ def toNat? (s : Substring) : Option Nat := if s.isNat then some <| s.foldl (fun n c => n*10 + (c.toNat - '0'.toNat)) 0 diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index d3e34a2a35..242fac8ee7 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -11,7 +11,14 @@ open Sum Subtype Nat open Std +/-- +Types that can be converted into a string for display. + +There is no expectation that the resulting string can be parsed back to the original data (see +`Repr` for a similar class with this expectation). +-/ class ToString (α : Type u) where + /-- Converts a value into a string. -/ toString : α → String export ToString (toString) diff --git a/src/Init/Dynamic.lean b/src/Init/Dynamic.lean index a784b7dc2c..f80e882808 100644 --- a/src/Init/Dynamic.lean +++ b/src/Init/Dynamic.lean @@ -57,10 +57,11 @@ private opaque DynamicPointed : NonemptyType.{0} := ⟨Name × NonScalar, inferInstance⟩ /-- -Type-tagged union that can store any type with a `TypeName` instance. +A type-tagged union that can store any type with a `TypeName` instance. -This is roughly equivalent to `(α : Type) × TypeName α × α` but without the -universe bump. +This is roughly equivalent to `(α : Type) × TypeName α × α`, but without the universe bump. Use +`Dynamic.mk` to inject a value into `Dynamic` from another type, and `Dynamic.get?` to extract a +value from `Dynamic` if it has some expected type. -/ def Dynamic : Type := DynamicPointed.type @@ -92,5 +93,10 @@ opaque Dynamic.get? (α) (any : Dynamic) [TypeName α] : Option α private unsafe def Dynamic.mkImpl [TypeName α] (obj : α) : Dynamic := unsafeCast (TypeName.typeName α, (unsafeCast obj : NonScalar)) +/-- +Stores the provided value in a `Dynamic`. + +Use `Dynamic.get? α` to retrieve it. +-/ @[implemented_by Dynamic.mkImpl] opaque Dynamic.mk [TypeName α] (obj : α) : Dynamic diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean index e05144ef7c..7978f6c86f 100644 --- a/src/Init/Internal/Order/Basic.lean +++ b/src/Init/Internal/Order/Basic.lean @@ -35,8 +35,11 @@ class PartialOrder (α : Sort u) where This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise. -/ rel : α → α → Prop + /-- The “less-or-equal-to” or “approximates” relation is reflexive. -/ rel_refl : ∀ {x}, rel x x + /-- The “less-or-equal-to” or “approximates” relation is transitive. -/ rel_trans : ∀ {x y z}, rel x y → rel y z → rel x z + /-- The “less-or-equal-to” or “approximates” relation is antisymmetric. -/ rel_antisymm : ∀ {x y}, rel x y → rel y x → x = y @[inherit_doc] scoped infix:50 " ⊑ " => PartialOrder.rel @@ -61,15 +64,21 @@ section CCPO /-- A chain-complete partial order (CCPO) is a partial order where every chain has a least upper bound. -This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise. +This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used +otherwise. -/ class CCPO (α : Sort u) extends PartialOrder α where /-- The least upper bound of a chain. - This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise. + This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used + otherwise. -/ csup : (α → Prop) → α + /-- + `csup c` is the least upper bound of the chain `c` when all elements `x` that are at + least as large as `csup c` are at least as large as all elements of `c`, and vice versa. + -/ csup_spec {c : α → Prop} (hc : chain c) : csup c ⊑ x ↔ (∀ y, c y → y ⊑ x) open PartialOrder CCPO diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 6418c0332c..3a3819b3ef 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1484,12 +1484,18 @@ structure ApplyConfig where namespace Rewrite +@[inherit_doc ApplyNewGoals] abbrev NewGoals := ApplyNewGoals +/-- Configures the behavior of the `rewrite` and `rw` tactics. -/ structure Config where + /-- The transparency mode to use for unfolding -/ transparency : TransparencyMode := .reducible + /-- Whether to support offset constraints such as `?x + 1 =?= e` -/ offsetCnstrs : Bool := true + /-- Which occurrences to rewrite-/ occs : Occurrences := .all + /-- How to convert the resulting metavariables into new goals -/ newGoals : NewGoals := .nonDependentFirst end Rewrite diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean index c122b2f90a..00b218ed01 100644 --- a/src/Init/MetaTypes.lean +++ b/src/Init/MetaTypes.lean @@ -20,17 +20,21 @@ structure Module where namespace Meta +/-- +Which constants should be unfolded? +-/ inductive TransparencyMode where - /-- unfold all constants, even those tagged as `@[irreducible]`. -/ + /-- Unfolds all constants, even those tagged as `@[irreducible]`. -/ | all - /-- unfold all constants except those tagged as `@[irreducible]`. -/ + /-- Unfolds all constants except those tagged as `@[irreducible]`. -/ | default - /-- unfold only constants tagged with the `@[reducible]` attribute. -/ + /-- Unfolds only constants tagged with the `@[reducible]` attribute. -/ | reducible - /-- unfold reducible constants and constants tagged with the `@[instance]` attribute. -/ + /-- Unfolds reducible constants and constants tagged with the `@[instance]` attribute. -/ | instances deriving Inhabited, BEq +/-- Which structure types should eta be used with? -/ inductive EtaStructMode where /-- Enable eta for structure and classes. -/ | all diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index 8b89b45840..8c41290bc5 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -17,6 +17,7 @@ Paths consist of a sequence of directories followed by the name of a file or dir delimited by a platform-dependent separator character (see `System.FilePath.pathSeparator`). -/ structure FilePath where + /-- The string representation of the path. -/ toString : String deriving Inhabited, DecidableEq, Hashable diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index f026bf8c25..7eae7c1d23 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -1482,8 +1482,11 @@ The `FileRight` structure describes these permissions for a file's owner, member group, and all others. -/ structure AccessRight where + /-- The file can be read. -/ read : Bool := false + /-- The file can be written to. -/ write : Bool := false + /-- The file can be executed. -/ execution : Bool := false /-- diff --git a/src/Init/Util.lean b/src/Init/Util.lean index 7011f4b0ea..5aa4b7bc2f 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -42,12 +42,19 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f () @[never_extract, inline] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α := panic (mkPanicMessageWithDecl modName declName line col msg) +/-- +Returns the address at which an object is allocated. + +This function is unsafe because it can distinguish between definitionally equal values. +-/ @[extern "lean_ptr_addr"] unsafe opaque ptrAddrUnsafe {α : Type u} (a : @& α) : USize /-- Returns `true` if `a` is an exclusive object. -We say an object is exclusive if it is single-threaded and its reference counter is 1. + +An object is exclusive if it is single-threaded and its reference counter is 1. This function is +unsafe because it can distinguish between definitionally equal values. -/ @[extern "lean_is_exclusive_obj"] unsafe opaque isExclusiveUnsafe {α : Type u} (a : @& α) : Bool @@ -56,8 +63,21 @@ set_option linter.unusedVariables.funArgs false in @[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k (ptrAddrUnsafe a) +/-- +Compares two objects for pointer equality. + +Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This +function is unsafe because it can distinguish between definitionally equal values. +-/ @[inline] unsafe def ptrEq (a b : α) : Bool := ptrAddrUnsafe a == ptrAddrUnsafe b +/-- +Compares two lists of objects for element-wise pointer equality. Returns `true` if both lists are +the same length and the objects at the corresponding indices of each list are pointer-equal. + +Two objects are pointer-equal if, at runtime, they are allocated at exactly the same address. This +function is unsafe because it can distinguish between definitionally equal values. +-/ unsafe def ptrEqList : (as bs : List α) → Bool | [], [] => true | a::as, b::bs => if ptrEq a b then ptrEqList as bs else false diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean index c2c9040c3f..a75f6dde0b 100644 --- a/src/lake/Lake/Config/LeanConfig.lean +++ b/src/lake/Lake/Config/LeanConfig.lean @@ -121,9 +121,11 @@ protected def BuildType.toString (bt : BuildType) : String := instance : ToString BuildType := ⟨BuildType.toString⟩ -/-- Option that is used by Lean as if it was passed using `-D`. -/ +/-- An option that is used by Lean as if it was passed using `-D`. -/ structure LeanOption where + /-- The option's name. -/ name : Lean.Name + /-- The option's value. -/ value : Lean.LeanOptionValue deriving Inhabited, Repr