chore: Grove: add some data (#9354)
This commit is contained in:
Markus Himmel
GitHub
parent
a7789d863c
commit
0931033c72
8 changed files with 1053 additions and 453 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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?"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@
|
|||
"type": "git",
|
||||
"subDir": "backend",
|
||||
"scope": "",
|
||||
"rev": "7c28641a900d7ab7197a4082fea11189586fe523",
|
||||
"rev": "73631df7077bbd1c7283da8f5165134a27d417fa",
|
||||
"name": "grove",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue