From 0931033c72fea3544133ae5bd86ec9953ae77313 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 14 Jul 2025 12:22:59 +0200 Subject: [PATCH] chore: Grove: add some data (#9354) --- doc/std/grove/GroveStdlib/Generated.lean | 8 + .../associative-all-operations-covered.lean | 34 + .../associative-create-then-query.lean | 357 ++++++++ .../associative-creation-operations.lean | 216 +++++ .../associative-modification-operations.lean | 21 + .../associative-query-operations.lean | 806 ++++++++---------- .../CoreTypesAndOperations/Containers.lean | 62 +- doc/std/grove/lake-manifest.json | 2 +- 8 files changed, 1053 insertions(+), 453 deletions(-) create mode 100644 doc/std/grove/GroveStdlib/Generated/associative-all-operations-covered.lean create mode 100644 doc/std/grove/GroveStdlib/Generated/associative-create-then-query.lean create mode 100644 doc/std/grove/GroveStdlib/Generated/associative-creation-operations.lean create mode 100644 doc/std/grove/GroveStdlib/Generated/associative-modification-operations.lean diff --git a/doc/std/grove/GroveStdlib/Generated.lean b/doc/std/grove/GroveStdlib/Generated.lean index 26b03b6f98..dc5d8e7036 100644 --- a/doc/std/grove/GroveStdlib/Generated.lean +++ b/doc/std/grove/GroveStdlib/Generated.lean @@ -1,5 +1,9 @@ import Grove.Framework import GroveStdlib.Generated.«associative-query-operations» +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» /- This file is autogenerated by grove. You can manually edit it, for example to resolve merge @@ -12,3 +16,7 @@ namespace GroveStdlib.Generated def restoreState : RestoreStateM Unit := do «associative-query-operations».restoreState + «associative-creation-operations».restoreState + «associative-modification-operations».restoreState + «associative-create-then-query».restoreState + «associative-all-operations-covered».restoreState diff --git a/doc/std/grove/GroveStdlib/Generated/associative-all-operations-covered.lean b/doc/std/grove/GroveStdlib/Generated/associative-all-operations-covered.lean new file mode 100644 index 0000000000..69af323b61 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Generated/associative-all-operations-covered.lean @@ -0,0 +1,34 @@ +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.«associative-all-operations-covered» + +def «all-covered» : Assertion.Fact where + widgetId := "associative-all-operations-covered" + factId := "all-covered" + assertionId := "all-covered" + state := { + assertionId := "all-covered" + description := "All operations should be covered" + passed := false + message := "There were 19697 operations that were not covered." + } + metadata := { + status := .bad + comment := "Still missing some!" + } + +def table : Assertion.Data where + widgetId := "associative-all-operations-covered" + facts := #[ + «all-covered», + ] + +def restoreState : RestoreStateM Unit := do + addAssertion table \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Generated/associative-create-then-query.lean b/doc/std/grove/GroveStdlib/Generated/associative-create-then-query.lean new file mode 100644 index 0000000000..677a77d66e --- /dev/null +++ b/doc/std/grove/GroveStdlib/Generated/associative-create-then-query.lean @@ -0,0 +1,357 @@ +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.«associative-create-then-query» + +def «2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where + widgetId := "associative-create-then-query" + factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap" + rowAssociationId := "2cb3c441-9663-4ce7-9527-0f40fc29925a" + columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ] + layerStates := #[ + { + layerIdentifier := "Std.DHashMap" + rowState := + + some ⟨"Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.emptyWithCapacity, + renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.DHashMap α β", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.isEmpty, + renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.DHashMap.Raw" + rowState := + + some ⟨"Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.emptyWithCapacity, + renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n Std.DHashMap.Raw α β", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.isEmpty, + renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.ExtDHashMap" + rowState := + + some ⟨"Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.emptyWithCapacity, + renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtDHashMap α β", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.isEmpty, + renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.DTreeMap" + rowState := + + some ⟨"Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.empty, + renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.DTreeMap α β cmp", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.isEmpty, + renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.DTreeMap.Raw" + rowState := + + some ⟨"Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.empty, + renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.DTreeMap.Raw α β cmp", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.isEmpty, + renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.ExtDTreeMap" + rowState := + + some ⟨"Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.empty, + renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.ExtDTreeMap α β cmp", + isDeprecated := false })⟩ + + columnState := + + some ⟨"Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.isEmpty, + renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + ] + metadata := { + status := .done + comment := "Not necessary for `ExtDHashMap` because of simp lemma turning into varno" + } + +def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap» : Table.Fact .subexpression .subexpression .declaration where + widgetId := "associative-create-then-query" + factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap" + rowAssociationId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnAssociationId := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ] + layerStates := #[ + { + layerIdentifier := "Std.DHashMap" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.isEmpty, + renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ⟨"Std.DHashMap.isEmpty_empty", Grove.Framework.Declaration.thm + { name := `Std.DHashMap.isEmpty_empty, + renderedStatement := "Std.DHashMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} :\n ∅.isEmpty = true", + isSimp := true, + isDeprecated := false }⟩ +, + ] + }, + { + layerIdentifier := "Std.DHashMap.Raw" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.isEmpty, + renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ⟨"Std.DHashMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm + { name := `Std.DHashMap.Raw.isEmpty_emptyc, + renderedStatement := "Std.DHashMap.Raw.isEmpty_emptyc.{u_1, u_2} {α : Type u_1} {β : α → Type u_2} [BEq α] [Hashable α] :\n ∅.isEmpty = true", + isSimp := false, + isDeprecated := true }⟩ +, + ] + }, + { + layerIdentifier := "Std.ExtDHashMap" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.isEmpty, + renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ] + }, + { + layerIdentifier := "Std.DTreeMap" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.isEmpty, + renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ⟨"Std.DTreeMap.isEmpty_emptyc", Grove.Framework.Declaration.thm + { name := `Std.DTreeMap.isEmpty_emptyc, + renderedStatement := "Std.DTreeMap.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n ∅.isEmpty = true", + isSimp := true, + isDeprecated := false }⟩ +, + ] + }, + { + layerIdentifier := "Std.DTreeMap.Raw" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.isEmpty, + renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ⟨"Std.DTreeMap.Raw.isEmpty_emptyc", Grove.Framework.Declaration.thm + { name := `Std.DTreeMap.Raw.isEmpty_emptyc, + renderedStatement := "Std.DTreeMap.Raw.isEmpty_emptyc.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n ∅.isEmpty = true", + isSimp := true, + isDeprecated := false }⟩ +, + ] + }, + { + layerIdentifier := "Std.ExtDTreeMap" + rowState := + + some ⟨"app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "∅" }⟩ + + columnState := + + some ⟨"Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.isEmpty, + renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool", + isDeprecated := false })⟩ + + selectedCellStates := #[ + ⟨"Std.ExtDTreeMap.isEmpty_empty", Grove.Framework.Declaration.thm + { name := `Std.ExtDTreeMap.isEmpty_empty, + renderedStatement := "Std.ExtDTreeMap.isEmpty_empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n ∅.isEmpty = true", + isSimp := true, + isDeprecated := false }⟩ +, + ] + }, + ] + metadata := { + status := .bad + comment := "Missing for `ExtDHashMap`" + } + +def table : Table.Data .subexpression .subexpression .declaration where + widgetId := "associative-create-then-query" + selectedRowAssociations := #["2cb3c441-9663-4ce7-9527-0f40fc29925a", "7743a485-024d-43b6-bd5f-ebd3182eb94d", "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", ] + selectedColumnAssociations := #["01f88623-fa5f-4380-9772-b30f2fec5c94", "f084f852-af71-45b6-8ab3-d251a8144f72", ] + selectedLayers := #["Std.DHashMap", "Std.DHashMap.Raw", "Std.ExtDHashMap", "Std.DTreeMap", "Std.DTreeMap.Raw", "Std.ExtDTreeMap", ] + selectedCellOptions := #[ + { + layerIdentifier := "Std.DHashMap" + rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DHashMap.isEmpty_emptyWithCapacity", ] + }, + { + layerIdentifier := "Std.DHashMap.Raw" + rowValue := "2cb3c441-9663-4ce7-9527-0f40fc29925a" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyWithCapacity", ] + }, + { + layerIdentifier := "Std.DHashMap" + rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DHashMap.isEmpty_empty", ] + }, + { + layerIdentifier := "Std.DHashMap.Raw" + rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DHashMap.Raw.isEmpty_emptyc", ] + }, + { + layerIdentifier := "Std.DTreeMap" + rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DTreeMap.isEmpty_emptyc", ] + }, + { + layerIdentifier := "Std.DTreeMap.Raw" + rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.DTreeMap.Raw.isEmpty_emptyc", ] + }, + { + layerIdentifier := "Std.ExtDTreeMap" + rowValue := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + columnValue := "01f88623-fa5f-4380-9772-b30f2fec5c94" + selectedCellOptions := #["Std.ExtDTreeMap.isEmpty_empty", ] + }, + ] + facts := #[ + «2cb3c441-9663-4ce7-9527-0f40fc29925a:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap», + «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d:::01f88623-fa5f-4380-9772-b30f2fec5c94:::Std.DHashMap::Std.DHashMap.Raw::Std.ExtDHashMap::Std.DTreeMap::Std.DTreeMap.Raw::Std.ExtDTreeMap», + ] + +def restoreState : RestoreStateM Unit := do + addTable table \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Generated/associative-creation-operations.lean b/doc/std/grove/GroveStdlib/Generated/associative-creation-operations.lean new file mode 100644 index 0000000000..d500292bbc --- /dev/null +++ b/doc/std/grove/GroveStdlib/Generated/associative-creation-operations.lean @@ -0,0 +1,216 @@ +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.«associative-creation-operations» + +def «2cb3c441-9663-4ce7-9527-0f40fc29925a» : AssociationTable.Fact .subexpression where + widgetId := "associative-creation-operations" + factId := "2cb3c441-9663-4ce7-9527-0f40fc29925a" + rowId := "2cb3c441-9663-4ce7-9527-0f40fc29925a" + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.emptyWithCapacity, + renderedStatement := "Std.DHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.DHashMap α β", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.emptyWithCapacity, + renderedStatement := "Std.DHashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} (capacity : Nat := 8) :\n Std.DHashMap.Raw α β", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.emptyWithCapacity, + renderedStatement := "Std.ExtDHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtDHashMap α β", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.empty, + renderedStatement := "Std.DTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.DTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.empty, + renderedStatement := "Std.DTreeMap.Raw.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.DTreeMap.Raw α β cmp", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.empty, + renderedStatement := "Std.ExtDTreeMap.empty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :\n Std.ExtDTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.emptyWithCapacity, + renderedStatement := "Std.HashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.HashMap α β", + isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.Raw.emptyWithCapacity, + renderedStatement := "Std.HashMap.Raw.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} (capacity : Nat := 8) :\n Std.HashMap.Raw α β", + isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashMap.emptyWithCapacity, + renderedStatement := "Std.ExtHashMap.emptyWithCapacity.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (capacity : Nat := 8) : Std.ExtHashMap α β", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.empty, + renderedStatement := "Std.TreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Std.TreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.empty, + renderedStatement := "Std.TreeMap.Raw.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} :\n Std.TreeMap.Raw α β cmp", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.empty, + renderedStatement := "Std.ExtTreeMap.empty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} :\n Std.ExtTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.emptyWithCapacity, + renderedStatement := "Std.HashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n Std.HashSet α", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.emptyWithCapacity, + renderedStatement := "Std.HashSet.Raw.emptyWithCapacity.{u} {α : Type u} (capacity : Nat := 8) : Std.HashSet.Raw α", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.emptyWithCapacity, + renderedStatement := "Std.ExtHashSet.emptyWithCapacity.{u} {α : Type u} [BEq α] [Hashable α] (capacity : Nat := 8) :\n Std.ExtHashSet α", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.empty, + renderedStatement := "Std.TreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.TreeSet α cmp", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.empty, + renderedStatement := "Std.TreeSet.Raw.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.TreeSet.Raw α cmp", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.empty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.empty, + renderedStatement := "Std.ExtTreeSet.empty.{u} {α : Type u} {cmp : α → α → Ordering} : Std.ExtTreeSet α cmp", + isDeprecated := false })⟩,] + metadata := { + status := .done + comment := "" + } +def «7743a485-024d-43b6-bd5f-ebd3182eb94d» : AssociationTable.Fact .subexpression where + widgetId := "associative-creation-operations" + factId := "7743a485-024d-43b6-bd5f-ebd3182eb94d" + rowId := "7743a485-024d-43b6-bd5f-ebd3182eb94d" + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.ofList, + renderedStatement := "Std.DHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.DHashMap α β", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.ofList, + renderedStatement := "Std.DHashMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.DHashMap.Raw α β", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.ofList, + renderedStatement := "Std.ExtDHashMap.ofList.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α]\n (l : List ((a : α) × β a)) : Std.ExtDHashMap α β", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.ofList, + renderedStatement := "Std.DTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : α → α → Ordering := by exact compare) : Std.DTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.ofList, + renderedStatement := "Std.DTreeMap.Raw.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : α → α → Ordering := by exact compare) : Std.DTreeMap.Raw α β cmp", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.ofList, + renderedStatement := "Std.ExtDTreeMap.ofList.{u, v} {α : Type u} {β : α → Type v} (l : List ((a : α) × β a))\n (cmp : α → α → Ordering := by exact compare) : Std.ExtDTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.ofList, + renderedStatement := "Std.HashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.HashMap α β", + isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.Raw.ofList, + renderedStatement := "Std.HashMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.HashMap.Raw α β", + isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashMap.ofList, + renderedStatement := "Std.ExtHashMap.ofList.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) :\n Std.ExtHashMap α β", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.ofList, + renderedStatement := "Std.TreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : α → α → Ordering := by exact compare) : Std.TreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.ofList, + renderedStatement := "Std.TreeMap.Raw.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : α → α → Ordering := by exact compare) : Std.TreeMap.Raw α β cmp", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.ofList, + renderedStatement := "Std.ExtTreeMap.ofList.{u, v} {α : Type u} {β : Type v} (l : List (α × β))\n (cmp : α → α → Ordering := by exact compare) : Std.ExtTreeMap α β cmp", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.ofList, + renderedStatement := "Std.HashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet α", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.ofList, + renderedStatement := "Std.HashSet.Raw.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.HashSet.Raw α", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.ofList, + renderedStatement := "Std.ExtHashSet.ofList.{u} {α : Type u} [BEq α] [Hashable α] (l : List α) : Std.ExtHashSet α", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.ofList, + renderedStatement := "Std.TreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n Std.TreeSet α cmp", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.ofList, + renderedStatement := "Std.TreeSet.Raw.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n Std.TreeSet.Raw α cmp", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.ofList", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.ofList, + renderedStatement := "Std.ExtTreeSet.ofList.{u} {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) :\n Std.ExtTreeSet α cmp", + isDeprecated := false })⟩,] + metadata := { + status := .done + comment := "" + } +def «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d» : AssociationTable.Fact .subexpression where + widgetId := "associative-creation-operations" + factId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + rowId := "5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d" + rowState := #[⟨"Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap*)", displayShort := "∅" }⟩,⟨"Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)", displayShort := "∅" }⟩,⟨"Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)", displayShort := "∅" }⟩,⟨"Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)", displayShort := "∅" }⟩,⟨"Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.HashMap*)", displayShort := "∅" }⟩,⟨"Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)", displayShort := "∅" }⟩,⟨"Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.TreeMap*)", displayShort := "∅" }⟩,⟨"Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)", displayShort := "∅" }⟩,⟨"Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.HashSet*)", displayShort := "∅" }⟩,⟨"Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)", displayShort := "∅" }⟩,⟨"Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.TreeSet*)", displayShort := "∅" }⟩,⟨"Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)", displayShort := "∅" }⟩,⟨"Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", Grove.Framework.Subexpression.State.predicate + { key := "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)", displayShort := "∅" }⟩,] + metadata := { + status := .done + comment := "" + } + +def table : AssociationTable.Data .subexpression where + widgetId := "associative-creation-operations" + rows := #[ + ⟨"2cb3c441-9663-4ce7-9527-0f40fc29925a", "empty", #[⟨"Std.DHashMap", "Std.DHashMap.emptyWithCapacity"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.emptyWithCapacity"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.emptyWithCapacity"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.empty"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.empty"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.empty"⟩,⟨"Std.HashMap", "Std.HashMap.emptyWithCapacity"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.emptyWithCapacity"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.emptyWithCapacity"⟩,⟨"Std.TreeMap", "Std.TreeMap.empty"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.empty"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.empty"⟩,⟨"Std.HashSet", "Std.HashSet.emptyWithCapacity"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.emptyWithCapacity"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.emptyWithCapacity"⟩,⟨"Std.TreeSet", "Std.TreeSet.empty"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.empty"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.empty"⟩,]⟩, + ⟨"7743a485-024d-43b6-bd5f-ebd3182eb94d", "ofList", #[⟨"Std.DHashMap", "Std.DHashMap.ofList"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.ofList"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.ofList"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.ofList"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.ofList"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.ofList"⟩,⟨"Std.HashMap", "Std.HashMap.ofList"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.ofList"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.ofList"⟩,⟨"Std.TreeMap", "Std.TreeMap.ofList"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.ofList"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.ofList"⟩,⟨"Std.HashSet", "Std.HashSet.ofList"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.ofList"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.ofList"⟩,⟨"Std.TreeSet", "Std.TreeSet.ofList"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.ofList"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.ofList"⟩,]⟩, + ⟨"5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d", "emptyCollection", #[⟨"Std.DHashMap", "app (EmptyCollection.emptyCollection) (Std.DHashMap*)"⟩,⟨"Std.DHashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DHashMap.Raw*)"⟩,⟨"Std.ExtDHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtDHashMap*)"⟩,⟨"Std.DTreeMap", "app (EmptyCollection.emptyCollection) (Std.DTreeMap*)"⟩,⟨"Std.DTreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.DTreeMap.Raw*)"⟩,⟨"Std.ExtDTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtDTreeMap*)"⟩,⟨"Std.HashMap", "app (EmptyCollection.emptyCollection) (Std.HashMap*)"⟩,⟨"Std.HashMap.Raw", "app (EmptyCollection.emptyCollection) (Std.HashMap.Raw*)"⟩,⟨"Std.ExtHashMap", "app (EmptyCollection.emptyCollection) (Std.ExtHashMap*)"⟩,⟨"Std.TreeMap", "app (EmptyCollection.emptyCollection) (Std.TreeMap*)"⟩,⟨"Std.TreeMap.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeMap.Raw*)"⟩,⟨"Std.ExtTreeMap", "app (EmptyCollection.emptyCollection) (Std.ExtTreeMap*)"⟩,⟨"Std.HashSet", "app (EmptyCollection.emptyCollection) (Std.HashSet*)"⟩,⟨"Std.HashSet.Raw", "app (EmptyCollection.emptyCollection) (Std.HashSet.Raw*)"⟩,⟨"Std.ExtHashSet", "app (EmptyCollection.emptyCollection) (Std.ExtHashSet*)"⟩,⟨"Std.TreeSet", "app (EmptyCollection.emptyCollection) (Std.TreeSet*)"⟩,⟨"Std.TreeSet.Raw", "app (EmptyCollection.emptyCollection) (Std.TreeSet.Raw*)"⟩,⟨"Std.ExtTreeSet", "app (EmptyCollection.emptyCollection) (Std.ExtTreeSet*)"⟩,]⟩, + ] + facts := #[ + «2cb3c441-9663-4ce7-9527-0f40fc29925a», + «7743a485-024d-43b6-bd5f-ebd3182eb94d», + «5ceaa26a-d2cb-4df3-9ac8-b5c11db2ae9d», + ] + +def restoreState : RestoreStateM Unit := do + addAssociationTable table \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Generated/associative-modification-operations.lean b/doc/std/grove/GroveStdlib/Generated/associative-modification-operations.lean new file mode 100644 index 0000000000..b5b25ca173 --- /dev/null +++ b/doc/std/grove/GroveStdlib/Generated/associative-modification-operations.lean @@ -0,0 +1,21 @@ +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.«associative-modification-operations» + + +def table : AssociationTable.Data .subexpression where + widgetId := "associative-modification-operations" + rows := #[ + ] + facts := #[ + ] + +def restoreState : RestoreStateM Unit := do + addAssociationTable table \ No newline at end of file diff --git a/doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean b/doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean index 9b165bc36c..13716f90bc 100644 --- a/doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean +++ b/doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean @@ -13,97 +13,79 @@ def «01f88623-fa5f-4380-9772-b30f2fec5c94» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "01f88623-fa5f-4380-9772-b30f2fec5c94" rowId := "01f88623-fa5f-4380-9772-b30f2fec5c94" - rowState := #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty", .declaration (Declaration.def { - name := `Std.DHashMap.isEmpty - renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.DHashMap.Raw.isEmpty - renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty", .declaration (Declaration.def { - name := `Std.ExtDHashMap.isEmpty - renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty", .declaration (Declaration.def { - name := `Std.DTreeMap.isEmpty - renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.isEmpty - renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.isEmpty - renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty", .declaration (Declaration.def { - name := `Std.HashMap.isEmpty - renderedStatement := "Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.HashMap.Raw.isEmpty - renderedStatement := "Std.HashMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty", .declaration (Declaration.def { - name := `Std.ExtHashMap.isEmpty - renderedStatement := "Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty", .declaration (Declaration.def { - name := `Std.TreeMap.isEmpty - renderedStatement := "Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.TreeMap.Raw.isEmpty - renderedStatement := "Std.TreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty", .declaration (Declaration.def { - name := `Std.ExtTreeMap.isEmpty - renderedStatement := "Std.ExtTreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty", .declaration (Declaration.def { - name := `Std.HashSet.isEmpty - renderedStatement := "Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.HashSet.Raw.isEmpty - renderedStatement := "Std.HashSet.Raw.isEmpty.{u} {α : Type u} (m : Std.HashSet.Raw α) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty", .declaration (Declaration.def { - name := `Std.ExtHashSet.isEmpty - renderedStatement := "Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashSet α) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty", .declaration (Declaration.def { - name := `Std.TreeSet.isEmpty - renderedStatement := "Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.isEmpty - renderedStatement := "Std.TreeSet.Raw.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty", .declaration (Declaration.def { - name := `Std.ExtTreeSet.isEmpty - renderedStatement := "Std.ExtTreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Bool" - isDeprecated := false - } -)⟩,] + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.isEmpty, + renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Bool", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.isEmpty, + renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.isEmpty, + renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.isEmpty, + renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.isEmpty, + renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.isEmpty, + renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.isEmpty, + renderedStatement := "Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Bool", + isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.Raw.isEmpty, + renderedStatement := "Std.HashMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashMap.isEmpty, + renderedStatement := "Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.isEmpty, + renderedStatement := "Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.isEmpty, + renderedStatement := "Std.TreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.isEmpty, + renderedStatement := "Std.ExtTreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.isEmpty, + renderedStatement := "Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.isEmpty, + renderedStatement := "Std.HashSet.Raw.isEmpty.{u} {α : Type u} (m : Std.HashSet.Raw α) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.isEmpty, + renderedStatement := "Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashSet α) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.isEmpty, + renderedStatement := "Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.isEmpty, + renderedStatement := "Std.TreeSet.Raw.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.isEmpty, + renderedStatement := "Std.ExtTreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Bool", + isDeprecated := false })⟩,] metadata := { status := .done comment := "" @@ -112,97 +94,79 @@ def «f084f852-af71-45b6-8ab3-d251a8144f72» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "f084f852-af71-45b6-8ab3-d251a8144f72" rowId := "f084f852-af71-45b6-8ab3-d251a8144f72" - rowState := #[⟨"Std.DHashMap", "Std.DHashMap.size", .declaration (Declaration.def { - name := `Std.DHashMap.size - renderedStatement := "Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size", .declaration (Declaration.def { - name := `Std.DHashMap.Raw.size - renderedStatement := "Std.DHashMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} (self : Std.DHashMap.Raw α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size", .declaration (Declaration.def { - name := `Std.ExtDHashMap.size - renderedStatement := "Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size", .declaration (Declaration.def { - name := `Std.DTreeMap.size - renderedStatement := "Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.size - renderedStatement := "Std.DTreeMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.size - renderedStatement := "Std.ExtDTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.HashMap", "Std.HashMap.size", .declaration (Declaration.def { - name := `Std.HashMap.size - renderedStatement := "Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size", .declaration (Declaration.def { - name := `Std.HashMap.Raw.size - renderedStatement := "Std.HashMap.Raw.size.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size", .declaration (Declaration.def { - name := `Std.ExtHashMap.size - renderedStatement := "Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap", "Std.TreeMap.size", .declaration (Declaration.def { - name := `Std.TreeMap.size - renderedStatement := "Std.TreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size", .declaration (Declaration.def { - name := `Std.TreeMap.Raw.size - renderedStatement := "Std.TreeMap.Raw.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size", .declaration (Declaration.def { - name := `Std.ExtTreeMap.size - renderedStatement := "Std.ExtTreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.HashSet", "Std.HashSet.size", .declaration (Declaration.def { - name := `Std.HashSet.size - renderedStatement := "Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size", .declaration (Declaration.def { - name := `Std.HashSet.Raw.size - renderedStatement := "Std.HashSet.Raw.size.{u} {α : Type u} (m : Std.HashSet.Raw α) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size", .declaration (Declaration.def { - name := `Std.ExtHashSet.size - renderedStatement := "Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.size", .declaration (Declaration.def { - name := `Std.TreeSet.size - renderedStatement := "Std.TreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.size - renderedStatement := "Std.TreeSet.Raw.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Nat" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size", .declaration (Declaration.def { - name := `Std.ExtTreeSet.size - renderedStatement := "Std.ExtTreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Nat" - isDeprecated := false - } -)⟩,] + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.size, + renderedStatement := "Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.DHashMap α β) : Nat", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.size, + renderedStatement := "Std.DHashMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} (self : Std.DHashMap.Raw α β) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.size, + renderedStatement := "Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [EquivBEq α] [LawfulHashable α] (m : Std.ExtDHashMap α β) : Nat", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.size, + renderedStatement := "Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.size, + renderedStatement := "Std.DTreeMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.size, + renderedStatement := "Std.ExtDTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.ExtDTreeMap α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.size, + renderedStatement := "Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) : Nat", + isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.Raw.size, + renderedStatement := "Std.HashMap.Raw.size.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashMap.size, + renderedStatement := "Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) : Nat", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.size, + renderedStatement := "Std.TreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.size, + renderedStatement := "Std.TreeMap.Raw.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.size, + renderedStatement := "Std.ExtTreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.ExtTreeMap α β cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.size, + renderedStatement := "Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Nat", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.size, + renderedStatement := "Std.HashSet.Raw.size.{u} {α : Type u} (m : Std.HashSet.Raw α) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.size, + renderedStatement := "Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) : Nat", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.size, + renderedStatement := "Std.TreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.size, + renderedStatement := "Std.TreeSet.Raw.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Nat", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.size, + renderedStatement := "Std.ExtTreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Nat", + isDeprecated := false })⟩,] metadata := { status := .done comment := "" @@ -211,62 +175,51 @@ def «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b" rowId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b" - rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.any", .declaration (Declaration.def { - name := `Std.DTreeMap.any - renderedStatement := "Std.DTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.any - renderedStatement := "Std.DTreeMap.Raw.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.any - renderedStatement := "Std.ExtDTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap", "Std.TreeMap.any", .declaration (Declaration.def { - name := `Std.TreeMap.any - renderedStatement := "Std.TreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any", .declaration (Declaration.def { - name := `Std.TreeMap.Raw.any - renderedStatement := "Std.TreeMap.Raw.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any", .declaration (Declaration.def { - name := `Std.ExtTreeMap.any - renderedStatement := "Std.ExtTreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet", "Std.HashSet.any", .declaration (Declaration.def { - name := `Std.HashSet.any - renderedStatement := "Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any", .declaration (Declaration.def { - name := `Std.HashSet.Raw.any - renderedStatement := "Std.HashSet.Raw.any.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.any", .declaration (Declaration.def { - name := `Std.TreeSet.any - renderedStatement := "Std.TreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.any - renderedStatement := "Std.TreeSet.Raw.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any", .declaration (Declaration.def { - name := `Std.ExtTreeSet.any - renderedStatement := "Std.ExtTreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,] + rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.any, + renderedStatement := "Std.DTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.any, + renderedStatement := "Std.DTreeMap.Raw.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.any, + renderedStatement := "Std.ExtDTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.any, + renderedStatement := "Std.TreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.any, + renderedStatement := "Std.TreeMap.Raw.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.any, + renderedStatement := "Std.ExtTreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.any, + renderedStatement := "Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.any, + renderedStatement := "Std.HashSet.Raw.any.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.any, + renderedStatement := "Std.TreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.any, + renderedStatement := "Std.TreeSet.Raw.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.any, + renderedStatement := "Std.ExtTreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool", + isDeprecated := false })⟩,] metadata := { status := .bad comment := "Missing for some containers" @@ -275,62 +228,51 @@ def «c1d181f6-3204-4956-946f-e81619f9feb4» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "c1d181f6-3204-4956-946f-e81619f9feb4" rowId := "c1d181f6-3204-4956-946f-e81619f9feb4" - rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.all", .declaration (Declaration.def { - name := `Std.DTreeMap.all - renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.all - renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.all - renderedStatement := "Std.ExtDTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap", "Std.TreeMap.all", .declaration (Declaration.def { - name := `Std.TreeMap.all - renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", .declaration (Declaration.def { - name := `Std.TreeMap.Raw.all - renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all", .declaration (Declaration.def { - name := `Std.ExtTreeMap.all - renderedStatement := "Std.ExtTreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet", "Std.HashSet.all", .declaration (Declaration.def { - name := `Std.HashSet.all - renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all", .declaration (Declaration.def { - name := `Std.HashSet.Raw.all - renderedStatement := "Std.HashSet.Raw.all.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.all", .declaration (Declaration.def { - name := `Std.TreeSet.all - renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.all - renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all", .declaration (Declaration.def { - name := `Std.ExtTreeSet.all - renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool" - isDeprecated := false - } -)⟩,] + rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.all, + renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.all, + renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n (t : Std.DTreeMap.Raw α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.all, + renderedStatement := "Std.ExtDTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.all, + renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.all, + renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.all, + renderedStatement := "Std.ExtTreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.all, + renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α)\n (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.all, + renderedStatement := "Std.HashSet.Raw.all.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.all, + renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) :\n Bool", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.all, + renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (p : α → Bool) : Bool", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.all, + renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (p : α → Bool) : Bool", + isDeprecated := false })⟩,] metadata := { status := .bad comment := "Missing for some containers" @@ -339,97 +281,79 @@ def «efe57f41-7db7-4303-b3a6-5216a70c43ce» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "efe57f41-7db7-4303-b3a6-5216a70c43ce" rowId := "efe57f41-7db7-4303-b3a6-5216a70c43ce" - rowState := #[⟨"Std.DHashMap", "Std.DHashMap.getD", .declaration (Declaration.def { - name := `Std.DHashMap.getD - renderedStatement := "Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD", .declaration (Declaration.def { - name := `Std.DHashMap.Raw.getD - renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]\n (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : β a" - isDeprecated := false - } -)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD", .declaration (Declaration.def { - name := `Std.ExtDHashMap.getD - renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD", .declaration (Declaration.def { - name := `Std.DTreeMap.getD - renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.getD - renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.getD - renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) :\n β a" - isDeprecated := false - } -)⟩,⟨"Std.HashMap", "Std.HashMap.getD", .declaration (Declaration.def { - name := `Std.HashMap.getD - renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD", .declaration (Declaration.def { - name := `Std.HashMap.Raw.getD - renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β)\n (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD", .declaration (Declaration.def { - name := `Std.ExtHashMap.getD - renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap", "Std.TreeMap.getD", .declaration (Declaration.def { - name := `Std.TreeMap.getD - renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", .declaration (Declaration.def { - name := `Std.TreeMap.Raw.getD - renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD", .declaration (Declaration.def { - name := `Std.ExtTreeMap.getD - renderedStatement := "Std.ExtTreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (a : α) (fallback : β) : β" - isDeprecated := false - } -)⟩,⟨"Std.HashSet", "Std.HashSet.getD", .declaration (Declaration.def { - name := `Std.HashSet.getD - renderedStatement := "Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a fallback : α) : α" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD", .declaration (Declaration.def { - name := `Std.HashSet.Raw.getD - renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α)\n (a fallback : α) : α" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD", .declaration (Declaration.def { - name := `Std.ExtHashSet.getD - renderedStatement := "Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a fallback : α) : α" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.getD", .declaration (Declaration.def { - name := `Std.TreeSet.getD - renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp)\n (a fallback : α) : α" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.getD - renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (a fallback : α) : α" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD", .declaration (Declaration.def { - name := `Std.ExtTreeSet.getD - renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a fallback : α) : α" - isDeprecated := false - } -)⟩,] + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.getD, + renderedStatement := "Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.getD, + renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α]\n (m : Std.DHashMap.Raw α β) (a : α) (fallback : β a) : β a", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.getD, + renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.getD, + renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.getD, + renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.getD, + renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) :\n β a", + isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.getD, + renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n (m : Std.HashMap α β) (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashMap.Raw.getD, + renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β)\n (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashMap.getD, + renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n [LawfulHashable α] (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.getD, + renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp)\n (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeMap.Raw.getD, + renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering}\n (t : Std.TreeMap.Raw α β cmp) (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeMap.getD, + renderedStatement := "Std.ExtTreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeMap α β cmp) (a : α) (fallback : β) : β", + isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.getD, + renderedStatement := "Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a fallback : α) : α", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.getD, + renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α)\n (a fallback : α) : α", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.getD, + renderedStatement := "Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a fallback : α) : α", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.getD, + renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp)\n (a fallback : α) : α", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.getD, + renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp)\n (a fallback : α) : α", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.getD, + renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a fallback : α) : α", + isDeprecated := false })⟩,] metadata := { status := .done comment := "" @@ -438,73 +362,61 @@ def «e23b1119-3b57-433e-a68d-68fd70b9943d» : AssociationTable.Fact .subexpress widgetId := "associative-query-operations" factId := "e23b1119-3b57-433e-a68d-68fd70b9943d" rowId := "e23b1119-3b57-433e-a68d-68fd70b9943d" - rowState := #[⟨"Std.DHashMap", "Std.DHashMap.get", .declaration (Declaration.def { - name := `Std.DHashMap.get - renderedStatement := "Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get", .declaration (Declaration.def { - name := `Std.DHashMap.Raw.Const.get - renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (m : Std.DHashMap.Raw α fun x => β) (a : α) (h : a ∈ m) : β" - isDeprecated := false - } -)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get", .declaration (Declaration.def { - name := `Std.ExtDHashMap.get - renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get", .declaration (Declaration.def { - name := `Std.DTreeMap.get - renderedStatement := "Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a" - isDeprecated := false - } -)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get", .declaration (Declaration.def { - name := `Std.DTreeMap.Raw.get - renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a" - isDeprecated := false - } -)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", .declaration (Declaration.def { - name := `Std.ExtDTreeMap.get - renderedStatement := "Std.ExtDTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β a" - isDeprecated := false - } -)⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate + rowState := #[⟨"Std.DHashMap", "Std.DHashMap.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.get, + renderedStatement := "Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : β a", + isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DHashMap.Raw.Const.get, + renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α]\n (m : Std.DHashMap.Raw α fun x => β) (a : α) (h : a ∈ m) : β", + isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDHashMap.get, + renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α}\n [LawfulBEq α] (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a", + isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.get, + renderedStatement := "Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a", + isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.DTreeMap.Raw.get, + renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}\n [Std.LawfulEqCmp cmp] (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a", + isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtDTreeMap.get, + renderedStatement := "Std.ExtDTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β a", + isDeprecated := false })⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate { key := "app (GetElem.getElem) (Std.HashMap*)", displayShort := "Std.HashMap[·]" }⟩,⟨"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate { key := "app (GetElem.getElem) (Std.HashMap.Raw*)", displayShort := "Std.HashMap.Raw[·]" }⟩,⟨"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate { key := "app (GetElem.getElem) (Std.ExtHashMap*)", displayShort := "Std.ExtHashMap[·]" }⟩,⟨"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate { key := "app (GetElem.getElem) (Std.TreeMap*)", displayShort := "Std.TreeMap[·]" }⟩,⟨"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate { key := "app (GetElem.getElem) (Std.TreeMap.Raw*)", displayShort := "Std.TreeMap.Raw[·]" }⟩,⟨"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate - { key := "app (GetElem.getElem) (Std.ExtTreeMap*)", displayShort := "Std.ExtTreeMap[·]" }⟩,⟨"Std.HashSet", "Std.HashSet.get", .declaration (Declaration.def { - name := `Std.HashSet.get - renderedStatement := "Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a : α) (h : a ∈ m) : α" - isDeprecated := false - } -)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get", .declaration (Declaration.def { - name := `Std.HashSet.Raw.get - renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α)\n (h : a ∈ m) : α" - isDeprecated := false - } -)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get", .declaration (Declaration.def { - name := `Std.ExtHashSet.get - renderedStatement := "Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a : α) (h : a ∈ m) : α" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet", "Std.TreeSet.get", .declaration (Declaration.def { - name := `Std.TreeSet.get - renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a : α)\n (h : a ∈ t) : α" - isDeprecated := false - } -)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", .declaration (Declaration.def { - name := `Std.TreeSet.Raw.get - renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α)\n (h : a ∈ t) : α" - isDeprecated := false - } -)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get", .declaration (Declaration.def { - name := `Std.ExtTreeSet.get - renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a : α) (h : a ∈ t) : α" - isDeprecated := false - } -)⟩,] + { key := "app (GetElem.getElem) (Std.ExtTreeMap*)", displayShort := "Std.ExtTreeMap[·]" }⟩,⟨"Std.HashSet", "Std.HashSet.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.get, + renderedStatement := "Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a : α) (h : a ∈ m) : α", + isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.HashSet.Raw.get, + renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α)\n (h : a ∈ m) : α", + isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtHashSet.get, + renderedStatement := "Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n (m : Std.ExtHashSet α) (a : α) (h : a ∈ m) : α", + isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.get, + renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a : α)\n (h : a ∈ t) : α", + isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.TreeSet.Raw.get, + renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α)\n (h : a ∈ t) : α", + isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get", Grove.Framework.Subexpression.State.declaration + (Grove.Framework.Declaration.def + { name := `Std.ExtTreeSet.get, + renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n (t : Std.ExtTreeSet α cmp) (a : α) (h : a ∈ t) : α", + isDeprecated := false })⟩,] metadata := { status := .bad comment := "Should *Set have GetElem?" diff --git a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean index 98440cc181..8ff63aa233 100644 --- a/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean +++ b/doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean @@ -20,10 +20,12 @@ def sequentialContainers : Node := namespace AssociativeContainers -def associativeQueryOperations : AssociationTable .subexpression - [`Std.DHashMap, `Std.DHashMap.Raw, `Std.ExtDHashMap, `Std.DTreeMap, `Std.DTreeMap.Raw, `Std.ExtDTreeMap, `Std.HashMap, - `Std.HashMap.Raw, `Std.ExtHashMap, `Std.TreeMap, `Std.TreeMap.Raw, `Std.ExtTreeMap, `Std.HashSet, `Std.HashSet.Raw, `Std.ExtHashSet, - `Std.TreeSet, `Std.TreeSet.Raw, `Std.ExtTreeSet] where +def associativeContainers : List Lean.Name := + [`Std.DHashMap, `Std.DHashMap.Raw, `Std.ExtDHashMap, `Std.DTreeMap, `Std.DTreeMap.Raw, `Std.ExtDTreeMap, `Std.HashMap, + `Std.HashMap.Raw, `Std.ExtHashMap, `Std.TreeMap, `Std.TreeMap.Raw, `Std.ExtTreeMap, `Std.HashSet, `Std.HashSet.Raw, `Std.ExtHashSet, + `Std.TreeSet, `Std.TreeSet.Raw, `Std.ExtTreeSet] + +def associativeQueryOperations : AssociationTable .subexpression associativeContainers where id := "associative-query-operations" title := "Associative query operations" description := "Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)." @@ -32,11 +34,61 @@ def associativeQueryOperations : AssociationTable .subexpression |>.map Subexpression.declaration |>.or (DataSource.getElem n) +def associativeCreationOperations : AssociationTable .subexpression associativeContainers where + id := "associative-creation-operations" + title := "Associative creation operations" + description := "Operations that create a new associative container" + dataSources n := + (DataSource.declarationsInNamespace n .definitionsOnly) + |>.map Subexpression.declaration + |>.or (DataSource.emptyCollection n) + +def associativeModificationOperations : AssociationTable .subexpression associativeContainers where + id := "associative-modification-operations" + title := "Associative modification operations" + description := "Operations that both accept and return an associative container" + dataSources n := + (DataSource.declarationsInNamespace n .definitionsOnly) + |>.map Subexpression.declaration + +def associativeCreateThenQuery : Table .subexpression .subexpression .declaration associativeContainers where + id := "associative-create-then-query" + title := "Associative create then query" + description := "Lemmas that say what happens when creating a new associative container and then immediately querying from it" + rowsFrom := .table associativeCreationOperations + columnsFrom := .table associativeQueryOperations + cellData := .classic _ { relevantNamespaces := associativeContainers } + +def allOperationsCovered : Assertion where + widgetId := "associative-all-operations-covered" + title := "All operations on associative containers covered" + description := "All operations on an associative container should appear in at least one of the tables" + check := do + let allValuesArray : Array String ← #[associativeQueryOperations, associativeCreationOperations, associativeModificationOperations].flatMapM valuesInAssociationTable + let allValues : Std.HashSet String := Std.HashSet.ofArray allValuesArray + let env ← Lean.getEnv + let mut numBad := 0 + for (n, _) in env.constants do + if associativeContainers.any (fun namesp => namesp.isPrefixOf n) then + if !n.toString ∈ allValues then + numBad := numBad + 1 + return #[{ + assertionId := "all-covered" + description := "All operations should be covered" + passed := numBad == 0 + message := if numBad = 0 then "All operations were covered" else s!"There were {numBad} operations that were not covered." + }] + end AssociativeContainers +open AssociativeContainers in def associativeContainers : Node := .section "associative-containers" "Associative containers" #[ - .associationTable AssociativeContainers.associativeQueryOperations + .associationTable associativeQueryOperations, + .associationTable associativeCreationOperations, + .associationTable associativeModificationOperations, + .table associativeCreateThenQuery, + .assertion allOperationsCovered ] namespace PersistentDataStructures diff --git a/doc/std/grove/lake-manifest.json b/doc/std/grove/lake-manifest.json index c30be05333..dcf9ca55c7 100644 --- a/doc/std/grove/lake-manifest.json +++ b/doc/std/grove/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": "backend", "scope": "", - "rev": "7c28641a900d7ab7197a4082fea11189586fe523", + "rev": "73631df7077bbd1c7283da8f5165134a27d417fa", "name": "grove", "manifestFile": "lake-manifest.json", "inputRev": "master",