doc: grove: update and add String data (#11551)

This PR bumps Grove to the latest revision and starts adding data about the `String` library. Just a small start, more to come.
2025-12-08 17:49:37 +01:00 · 2025-12-08 17:49:37 +01:00 · 3c100ada2a
commit 3c100ada2a
parent 383c0caa91
7 changed files with 489 additions and 7 deletions
--- a/.gitattributes
+++ b/.gitattributes
@ -4,6 +4,7 @@ RELEASES.md merge=union
 stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
+doc/std/grove/GroveStdlib/Generated/** linguist-generated
 # These files should not have line endings translated on Windows, because
 # it throws off parser tests. Later lines override earlier ones, so the
 # runner code is still treated as ordinary text.
--- a/.github/workflows/grove.yml
+++ b/.github/workflows/grove.yml
@ -65,6 +65,7 @@ jobs:
          workflow: ci.yml
          path: artifacts
          name: "build-Linux release"
+          allow_forks: true
          name_is_regexp: true

      - name: Unpack toolchain
--- a/doc/std/grove/GroveStdlib/Generated.lean
+++ b/doc/std/grove/GroveStdlib/Generated.lean
@ -4,6 +4,7 @@ import GroveStdlib.Generated.«associative-creation-operations»
 import GroveStdlib.Generated.«associative-modification-operations»
 import GroveStdlib.Generated.«associative-create-then-query»
 import GroveStdlib.Generated.«associative-all-operations-covered»
+import GroveStdlib.Generated.«slice-producing»

 /-
 This file is autogenerated by grove. You can manually edit it, for example to resolve merge
@ -20,3 +21,4 @@ def restoreState : RestoreStateM Unit := do
  «associative-modification-operations».restoreState
  «associative-create-then-query».restoreState
  «associative-all-operations-covered».restoreState
+  «slice-producing».restoreState
--- a/doc/std/grove/GroveStdlib/Generated/slice-producing.lean
+++ b/doc/std/grove/GroveStdlib/Generated/slice-producing.lean
@ -0,0 +1,459 @@
+import Grove.Framework
+
+/-
+This file is autogenerated by grove. You can manually edit it, for example to resolve merge
+conflicts, but be careful.
+-/
+
+open Grove.Framework Widget
+
+namespace GroveStdlib.Generated.«slice-producing»
+
+def «c8a13d6d-7ed6-4cd1-a386-23e2d55ce6f7» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "c8a13d6d-7ed6-4cd1-a386-23e2d55ce6f7"
+  rowId := "c8a13d6d-7ed6-4cd1-a386-23e2d55ce6f7"
+  rowState := #[⟨"String", "String.slice", Declaration.def {
+    name := `String.slice
+    renderedStatement := "String.slice (s : String) (startInclusive endExclusive : s.Pos)\n  (h : startInclusive ≤ endExclusive) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.slice", Declaration.def {
+    name := `String.Slice.slice
+    renderedStatement := "String.Slice.slice (s : String.Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd) :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-forwards", "String.Pos.slice", Declaration.def {
+    name := `String.Pos.slice
+    renderedStatement := "String.Pos.slice {s : String} (pos p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) :\n  (s.slice p₀ p₁ ⋯).Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-backwards", "String.Pos.ofSlice", Declaration.def {
+    name := `String.Pos.ofSlice
+    renderedStatement := "String.Pos.ofSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos : (s.slice p₀ p₁ h).Pos) : s.Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.slice", Declaration.def {
+    name := `String.Slice.Pos.slice
+    renderedStatement := "String.Slice.Pos.slice {s : String.Slice} (pos p₀ p₁ : s.Pos) (h₁ : p₀ ≤ pos) (h₂ : pos ≤ p₁) :\n  (s.slice p₀ p₁ ⋯).Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofSlice", Declaration.def {
+    name := `String.Slice.Pos.ofSlice
+    renderedStatement := "String.Slice.Pos.ofSlice {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}\n  (pos : (s.slice p₀ p₁ h).Pos) : s.Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-noproof", "String.Pos.sliceOrPanic", Declaration.def {
+    name := `String.Pos.sliceOrPanic
+    renderedStatement := "String.Pos.sliceOrPanic {s : String} (pos p₀ p₁ : s.Pos) {h : p₀ ≤ p₁} : (s.slice p₀ p₁ h).Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-noproof", "String.Slice.Pos.sliceOrPanic", Declaration.def {
+    name := `String.Slice.Pos.sliceOrPanic
+    renderedStatement := "String.Slice.Pos.sliceOrPanic {s : String.Slice} (pos p₀ p₁ : s.Pos) {h : p₀ ≤ p₁} :\n  (s.slice p₀ p₁ h).Pos"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .done
+    comment := ""
+  }
+def «21b4fdfd-f8b3-44f5-a59e-57f1dc1d6819» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "21b4fdfd-f8b3-44f5-a59e-57f1dc1d6819"
+  rowId := "21b4fdfd-f8b3-44f5-a59e-57f1dc1d6819"
+  rowState := #[⟨"String", "String.slice?", Declaration.def {
+    name := `String.slice?
+    renderedStatement := "String.slice? (s : String) (startInclusive endExclusive : s.Pos) : Option String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.slice?", Declaration.def {
+    name := `String.Slice.slice?
+    renderedStatement := "String.Slice.slice? (s : String.Slice) (newStart newEnd : s.Pos) : Option String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .postponed
+    comment := "Would be good to have better support"
+  }
+def «6f2b6ecb-2f0c-4e45-9da3-eb7f2e15eff0» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "6f2b6ecb-2f0c-4e45-9da3-eb7f2e15eff0"
+  rowId := "6f2b6ecb-2f0c-4e45-9da3-eb7f2e15eff0"
+  rowState := #[⟨"String", "String.slice!", Declaration.def {
+    name := `String.slice!
+    renderedStatement := "String.slice! (s : String) (p₁ p₂ : s.Pos) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.slice!", Declaration.def {
+    name := `String.Slice.slice!
+    renderedStatement := "String.Slice.slice! (s : String.Slice) (newStart newEnd : s.Pos) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-forwards", "String.Pos.slice!", Declaration.def {
+    name := `String.Pos.slice!
+    renderedStatement := "String.Pos.slice! {s : String} (pos p₀ p₁ : s.Pos) : (s.slice! p₀ p₁).Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-backwards", "String.Pos.ofSlice!", Declaration.def {
+    name := `String.Pos.ofSlice!
+    renderedStatement := "String.Pos.ofSlice! {s : String} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.slice!", Declaration.def {
+    name := `String.Slice.Pos.slice!
+    renderedStatement := "String.Slice.Pos.slice! {s : String.Slice} (pos p₀ p₁ : s.Pos) : (s.slice! p₀ p₁).Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofSlice!", Declaration.def {
+    name := `String.Slice.Pos.ofSlice!
+    renderedStatement := "String.Slice.Pos.ofSlice! {s : String.Slice} {p₀ p₁ : s.Pos} (pos : (s.slice! p₀ p₁).Pos) : s.Pos"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .done
+    comment := ""
+  }
+def «a3bdf66d-bc11-4019-aee9-2f1c1701de52» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "a3bdf66d-bc11-4019-aee9-2f1c1701de52"
+  rowId := "a3bdf66d-bc11-4019-aee9-2f1c1701de52"
+  rowState := #[⟨"String", "String.trimAsciiStart", Declaration.def {
+    name := `String.trimAsciiStart
+    renderedStatement := "String.trimAsciiStart (s : String) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.trimAsciiStart", Declaration.def {
+    name := `String.Slice.trimAsciiStart
+    renderedStatement := "String.Slice.trimAsciiStart (s : String.Slice) : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing `of` version at least"
+  }
+def «f12b2730-7a4d-465c-8a6d-9d051c300fd5» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "f12b2730-7a4d-465c-8a6d-9d051c300fd5"
+  rowId := "f12b2730-7a4d-465c-8a6d-9d051c300fd5"
+  rowState := #[⟨"String", "String.trimAsciiEnd", Declaration.def {
+    name := `String.trimAsciiEnd
+    renderedStatement := "String.trimAsciiEnd (s : String) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.trimAsciiEnd", Declaration.def {
+    name := `String.Slice.trimAsciiEnd
+    renderedStatement := "String.Slice.trimAsciiEnd (s : String.Slice) : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing `of` version at least"
+  }
+def «32307b55-d6d1-4756-a947-dbe4dfde573c» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "32307b55-d6d1-4756-a947-dbe4dfde573c"
+  rowId := "32307b55-d6d1-4756-a947-dbe4dfde573c"
+  rowState := #[⟨"String", "String.trimAscii", Declaration.def {
+    name := `String.trimAscii
+    renderedStatement := "String.trimAscii (s : String) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.trimAscii", Declaration.def {
+    name := `String.Slice.trimAscii
+    renderedStatement := "String.Slice.trimAscii (s : String.Slice) : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing `of` version at least\n"
+  }
+def «dce95a38-f55a-4d6a-ae79-078ffe4b5c15» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "dce95a38-f55a-4d6a-ae79-078ffe4b5c15"
+  rowId := "dce95a38-f55a-4d6a-ae79-078ffe4b5c15"
+  rowState := #[⟨"String", "String.toSlice", Declaration.def {
+    name := `String.toSlice
+    renderedStatement := "String.toSlice (s : String) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-forwards", "String.Pos.toSlice", Declaration.def {
+    name := `String.Pos.toSlice
+    renderedStatement := "String.Pos.toSlice {s : String} (pos : s.Pos) : s.toSlice.Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-pos-backwards", "String.Pos.ofToSlice", Declaration.def {
+    name := `String.Pos.ofToSlice
+    renderedStatement := "String.Pos.ofToSlice {s : String} (pos : s.toSlice.Pos) : s.Pos"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .done
+    comment := ""
+  }
+def «005a3f30-5dab-493f-b168-32c36a2bdf7c» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "005a3f30-5dab-493f-b168-32c36a2bdf7c"
+  rowId := "005a3f30-5dab-493f-b168-32c36a2bdf7c"
+  rowState := #[⟨"String.Slice", "String.Slice.str", Declaration.def {
+    name := `String.Slice.str
+    renderedStatement := "String.Slice.str (self : String.Slice) : String"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.str", Declaration.def {
+    name := `String.Slice.Pos.str
+    renderedStatement := "String.Slice.Pos.str {s : String.Slice} (pos : s.Pos) : s.str.Pos"
+    isDeprecated := false
+  }
+⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofStr", Declaration.def {
+    name := `String.Slice.Pos.ofStr
+    renderedStatement := "String.Slice.Pos.ofStr {s : String.Slice} (pos : s.str.Pos) (h₁ : s.startInclusive ≤ pos)\n  (h₂ : pos ≤ s.endExclusive) : s.Pos"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing `no proof` version\n"
+  }
+def «5f1a154c-ae2f-43a1-9409-2ce95b163ef3» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "5f1a154c-ae2f-43a1-9409-2ce95b163ef3"
+  rowId := "5f1a154c-ae2f-43a1-9409-2ce95b163ef3"
+  rowState := #[⟨"String", "String.drop", Declaration.def {
+    name := `String.drop
+    renderedStatement := "String.drop (s : String) (n : Nat) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.drop", Declaration.def {
+    name := `String.Slice.drop
+    renderedStatement := "String.Slice.drop (s : String.Slice) (n : Nat) : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «179518d1-ad07-4b2b-8ffe-3b7616e4c4ab» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "179518d1-ad07-4b2b-8ffe-3b7616e4c4ab"
+  rowId := "179518d1-ad07-4b2b-8ffe-3b7616e4c4ab"
+  rowState := #[⟨"String", "String.take", Declaration.def {
+    name := `String.take
+    renderedStatement := "String.take (s : String) (n : Nat) : String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.take", Declaration.def {
+    name := `String.Slice.take
+    renderedStatement := "String.Slice.take (s : String.Slice) (n : Nat) : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «55c587fd-a7a8-4633-a4ae-e2c4e768ad28» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "55c587fd-a7a8-4633-a4ae-e2c4e768ad28"
+  rowId := "55c587fd-a7a8-4633-a4ae-e2c4e768ad28"
+  rowState := #[⟨"String", "String.dropWhile", Declaration.def {
+    name := `String.dropWhile
+    renderedStatement := "String.dropWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropWhile", Declaration.def {
+    name := `String.Slice.dropWhile
+    renderedStatement := "String.Slice.dropWhile {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.ForwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «d4444684-4279-4400-9be2-561a7cdb32c1» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "d4444684-4279-4400-9be2-561a7cdb32c1"
+  rowId := "d4444684-4279-4400-9be2-561a7cdb32c1"
+  rowState := #[⟨"String", "String.takeWhile", Declaration.def {
+    name := `String.takeWhile
+    renderedStatement := "String.takeWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.takeWhile", Declaration.def {
+    name := `String.Slice.takeWhile
+    renderedStatement := "String.Slice.takeWhile {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.ForwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «1c9e6689-65a0-4d4b-b001-256e83917d98» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "1c9e6689-65a0-4d4b-b001-256e83917d98"
+  rowId := "1c9e6689-65a0-4d4b-b001-256e83917d98"
+  rowState := #[⟨"String", "String.dropEndWhile", Declaration.def {
+    name := `String.dropEndWhile
+    renderedStatement := "String.dropEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropEndWhile", Declaration.def {
+    name := `String.Slice.dropEndWhile
+    renderedStatement := "String.Slice.dropEndWhile {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.BackwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «b836052b-3470-4a8e-8989-6951c898de37» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "b836052b-3470-4a8e-8989-6951c898de37"
+  rowId := "b836052b-3470-4a8e-8989-6951c898de37"
+  rowState := #[⟨"String", "String.takeEndWhile", Declaration.def {
+    name := `String.takeEndWhile
+    renderedStatement := "String.takeEndWhile {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.takeEndWhile", Declaration.def {
+    name := `String.Slice.takeEndWhile
+    renderedStatement := "String.Slice.takeEndWhile {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.BackwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «5aa777d8-9642-43d8-9e20-30400fb8bb9d» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "5aa777d8-9642-43d8-9e20-30400fb8bb9d"
+  rowId := "5aa777d8-9642-43d8-9e20-30400fb8bb9d"
+  rowState := #[⟨"String", "String.dropPrefix", Declaration.def {
+    name := `String.dropPrefix
+    renderedStatement := "String.dropPrefix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropPrefix", Declaration.def {
+    name := `String.Slice.dropPrefix
+    renderedStatement := "String.Slice.dropPrefix {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.ForwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «80e3869d-fcfe-459d-8433-fe221f7b3c7a» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "80e3869d-fcfe-459d-8433-fe221f7b3c7a"
+  rowId := "80e3869d-fcfe-459d-8433-fe221f7b3c7a"
+  rowState := #[⟨"String", "String.dropSuffix", Declaration.def {
+    name := `String.dropSuffix
+    renderedStatement := "String.dropSuffix {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] :\n  String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropSuffix", Declaration.def {
+    name := `String.Slice.dropSuffix
+    renderedStatement := "String.Slice.dropSuffix {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.BackwardPattern pat] : String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .bad
+    comment := "Missing position transformations"
+  }
+def «4feda3e0-903b-4d52-b34e-0af70f7866e0» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "4feda3e0-903b-4d52-b34e-0af70f7866e0"
+  rowId := "4feda3e0-903b-4d52-b34e-0af70f7866e0"
+  rowState := #[⟨"String", "String.dropPrefix?", Declaration.def {
+    name := `String.dropPrefix?
+    renderedStatement := "String.dropPrefix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.ForwardPattern pat] :\n  Option String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropPrefix?", Declaration.def {
+    name := `String.Slice.dropPrefix?
+    renderedStatement := "String.Slice.dropPrefix? {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.ForwardPattern pat] : Option String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .postponed
+    comment := "Missing position transformations"
+  }
+def «45ca44c8-fbd5-4400-8297-a60778f302b0» : AssociationTable.Fact .declaration where
+  widgetId := "slice-producing"
+  factId := "45ca44c8-fbd5-4400-8297-a60778f302b0"
+  rowId := "45ca44c8-fbd5-4400-8297-a60778f302b0"
+  rowState := #[⟨"String", "String.dropSuffix?", Declaration.def {
+    name := `String.dropSuffix?
+    renderedStatement := "String.dropSuffix? {ρ : Type} (s : String) (pat : ρ) [String.Slice.Pattern.BackwardPattern pat] :\n  Option String.Slice"
+    isDeprecated := false
+  }
+⟩,⟨"String.Slice", "String.Slice.dropSuffix?", Declaration.def {
+    name := `String.Slice.dropSuffix?
+    renderedStatement := "String.Slice.dropSuffix? {ρ : Type} (s : String.Slice) (pat : ρ)\n  [String.Slice.Pattern.BackwardPattern pat] : Option String.Slice"
+    isDeprecated := false
+  }
+⟩,]
+  metadata := {
+    status := .postponed
+    comment := "Missing position transformations"
+  }
+
+def table : AssociationTable.Data .declaration where
+  widgetId := "slice-producing"
+  rows := #[
+    ⟨"c8a13d6d-7ed6-4cd1-a386-23e2d55ce6f7", "slice", #[⟨"String", "String.slice"⟩,⟨"String.Slice", "String.Slice.slice"⟩,⟨"string-pos-forwards", "String.Pos.slice"⟩,⟨"string-pos-backwards", "String.Pos.ofSlice"⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.slice"⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofSlice"⟩,⟨"string-pos-noproof", "String.Pos.sliceOrPanic"⟩,⟨"string-slice-pos-noproof", "String.Slice.Pos.sliceOrPanic"⟩,]⟩,
+    ⟨"21b4fdfd-f8b3-44f5-a59e-57f1dc1d6819", "slice?", #[⟨"String", "String.slice?"⟩,⟨"String.Slice", "String.Slice.slice?"⟩,]⟩,
+    ⟨"6f2b6ecb-2f0c-4e45-9da3-eb7f2e15eff0", "slice!", #[⟨"String", "String.slice!"⟩,⟨"String.Slice", "String.Slice.slice!"⟩,⟨"string-pos-forwards", "String.Pos.slice!"⟩,⟨"string-pos-backwards", "String.Pos.ofSlice!"⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.slice!"⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofSlice!"⟩,]⟩,
+    ⟨"a3bdf66d-bc11-4019-aee9-2f1c1701de52", "trimAsciiStart", #[⟨"String", "String.trimAsciiStart"⟩,⟨"String.Slice", "String.Slice.trimAsciiStart"⟩,]⟩,
+    ⟨"f12b2730-7a4d-465c-8a6d-9d051c300fd5", "trimAsciiEnd", #[⟨"String", "String.trimAsciiEnd"⟩,⟨"String.Slice", "String.Slice.trimAsciiEnd"⟩,]⟩,
+    ⟨"32307b55-d6d1-4756-a947-dbe4dfde573c", "trimAscii", #[⟨"String", "String.trimAscii"⟩,⟨"String.Slice", "String.Slice.trimAscii"⟩,]⟩,
+    ⟨"dce95a38-f55a-4d6a-ae79-078ffe4b5c15", "toSlice", #[⟨"String", "String.toSlice"⟩,⟨"string-pos-forwards", "String.Pos.toSlice"⟩,⟨"string-pos-backwards", "String.Pos.ofToSlice"⟩,]⟩,
+    ⟨"005a3f30-5dab-493f-b168-32c36a2bdf7c", "str", #[⟨"String.Slice", "String.Slice.str"⟩,⟨"string-slice-pos-forwards", "String.Slice.Pos.str"⟩,⟨"string-slice-pos-backwards", "String.Slice.Pos.ofStr"⟩,]⟩,
+    ⟨"5f1a154c-ae2f-43a1-9409-2ce95b163ef3", "drop", #[⟨"String", "String.drop"⟩,⟨"String.Slice", "String.Slice.drop"⟩,]⟩,
+    ⟨"179518d1-ad07-4b2b-8ffe-3b7616e4c4ab", "take", #[⟨"String", "String.take"⟩,⟨"String.Slice", "String.Slice.take"⟩,]⟩,
+    ⟨"55c587fd-a7a8-4633-a4ae-e2c4e768ad28", "dropWhile", #[⟨"String", "String.dropWhile"⟩,⟨"String.Slice", "String.Slice.dropWhile"⟩,]⟩,
+    ⟨"d4444684-4279-4400-9be2-561a7cdb32c1", "takeWhile", #[⟨"String", "String.takeWhile"⟩,⟨"String.Slice", "String.Slice.takeWhile"⟩,]⟩,
+    ⟨"1c9e6689-65a0-4d4b-b001-256e83917d98", "dropEndWhile", #[⟨"String", "String.dropEndWhile"⟩,⟨"String.Slice", "String.Slice.dropEndWhile"⟩,]⟩,
+    ⟨"b836052b-3470-4a8e-8989-6951c898de37", "takeEndWhile", #[⟨"String", "String.takeEndWhile"⟩,⟨"String.Slice", "String.Slice.takeEndWhile"⟩,]⟩,
+    ⟨"5aa777d8-9642-43d8-9e20-30400fb8bb9d", "dropPrefix", #[⟨"String", "String.dropPrefix"⟩,⟨"String.Slice", "String.Slice.dropPrefix"⟩,]⟩,
+    ⟨"80e3869d-fcfe-459d-8433-fe221f7b3c7a", "dropSuffix", #[⟨"String", "String.dropSuffix"⟩,⟨"String.Slice", "String.Slice.dropSuffix"⟩,]⟩,
+    ⟨"4feda3e0-903b-4d52-b34e-0af70f7866e0", "dropPrefix?", #[⟨"String", "String.dropPrefix?"⟩,⟨"String.Slice", "String.Slice.dropPrefix?"⟩,]⟩,
+    ⟨"45ca44c8-fbd5-4400-8297-a60778f302b0", "dropSuffix?", #[⟨"String", "String.dropSuffix?"⟩,⟨"String.Slice", "String.Slice.dropSuffix?"⟩,]⟩,
+  ]
+  facts := #[
+    «c8a13d6d-7ed6-4cd1-a386-23e2d55ce6f7»,
+    «21b4fdfd-f8b3-44f5-a59e-57f1dc1d6819»,
+    «6f2b6ecb-2f0c-4e45-9da3-eb7f2e15eff0»,
+    «a3bdf66d-bc11-4019-aee9-2f1c1701de52»,
+    «f12b2730-7a4d-465c-8a6d-9d051c300fd5»,
+    «32307b55-d6d1-4756-a947-dbe4dfde573c»,
+    «dce95a38-f55a-4d6a-ae79-078ffe4b5c15»,
+    «005a3f30-5dab-493f-b168-32c36a2bdf7c»,
+    «5f1a154c-ae2f-43a1-9409-2ce95b163ef3»,
+    «179518d1-ad07-4b2b-8ffe-3b7616e4c4ab»,
+    «55c587fd-a7a8-4633-a4ae-e2c4e768ad28»,
+    «d4444684-4279-4400-9be2-561a7cdb32c1»,
+    «1c9e6689-65a0-4d4b-b001-256e83917d98»,
+    «b836052b-3470-4a8e-8989-6951c898de37»,
+    «5aa777d8-9642-43d8-9e20-30400fb8bb9d»,
+    «80e3869d-fcfe-459d-8433-fe221f7b3c7a»,
+    «4feda3e0-903b-4d52-b34e-0af70f7866e0»,
+    «45ca44c8-fbd5-4400-8297-a60778f302b0»,
+  ]
+
+def restoreState : RestoreStateM Unit := do
+  addAssociationTable table
--- a/doc/std/grove/GroveStdlib/Std.lean
+++ b/doc/std/grove/GroveStdlib/Std.lean
@ -15,7 +15,7 @@ namespace GroveStdlib
 namespace Std

 def introduction : Node :=
-  .text "Welcome to the interactive Lean standard library outline!"
+  .text ⟨"introduction", "Welcome to the interactive Lean standard library outline!"⟩

 end Std

--- a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean
+++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean
@ -11,9 +11,28 @@ namespace GroveStdlib.Std.CoreTypesAndOperations

 namespace StringsAndFormatting

+def highLevelStringTypes : List Lean.Name :=
+  [`String, `String.Slice, `String.Pos, `String.Slice.Pos]
+
+def sliceProducing : AssociationTable (β := Alias Lean.Name) .declaration
+    [`String, `String.Slice,
+     Alias.mk `String.Pos "string-pos-forwards" "String.Pos (forwards)",
+     Alias.mk `String.Pos "string-pos-backwards" "String.Pos (backwards)",
+     Alias.mk `String.Pos "string-pos-noproof" "String.Pos (no proof)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-forwards" "String.Slice.Pos (forwards)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-backwards" "String.Slice.Pos (backwards)",
+     Alias.mk `String.Slice.Pos "string-slice-pos-noproof" "String.Slice.Pos (no proof)"] where
+  id := "slice-producing"
+  title := "String functions returning slices"
+  description := "Operations on strings and string slices that themselves return a new string slice."
+  dataSources n := DataSource.definitionsInNamespace n.inner
+
 end StringsAndFormatting

-def stringsAndFormatting : Node :=
-  .section "strings-and-formatting" "Strings and formatting" #[]
+open StringsAndFormatting

-end GroveStdlib.Std.CoreTypesAndOperations
+def stringsAndFormatting : Node :=
+  .section "strings-and-formatting" "Strings and formatting"
+    #[.associationTable sliceProducing]
+
+end GroveStdlib.Std.CoreTypesAndOperations
--- a/doc/std/grove/lake-manifest.json
+++ b/doc/std/grove/lake-manifest.json
@ -5,7 +5,7 @@
   "type": "git",
   "subDir": "backend",
   "scope": "",
-   "rev": "3e8aabdea58c11813c5d3b7eeb187ded44ee9a34",
+   "rev": "c19abde9101b29eb1e30d0d9d9e24ec2714f25b6",
   "name": "grove",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
@ -15,10 +15,10 @@
   "type": "git",
   "subDir": null,
   "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
+   "rev": "d9fc8ae23024be37424a189982c92356e37935c8",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
   "inherited": true,
   "configFile": "lakefile.toml"}],
 "name": "grovestdlib",