3c100ada2a
This PR bumps Grove to the latest revision and starts adding data about the `String` library. Just a small start, more to come.
459 lines
No EOL
22 KiB
Text
Generated
459 lines
No EOL
22 KiB
Text
Generated
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 |