| Metric | Count |
|---|
DefinitionsRBColor, Keys, next?, toArray, toList, toStream, Values, next?, toArray, toList, toStream, all, all₂, any, contains, empty, eqKeys, erase, filter, find!, find?, findD, findEntry?, foldl, foldlM, foldr, forM, insert, instBEq, instCoeHeadKeysArray, instCoeHeadKeysList, instCoeHeadValuesArray, instCoeHeadValuesList, instForInKeysOfMonad, instForInProdOfMonad, instForInValuesOfMonad, instForMKeysOfMonad, instForMValuesOfMonad, instRepr, instStreamStream, instStreamStream_1, instToStreamKeysStream, instToStreamStreamProd, instToStreamValuesStream, intersectWith, isEmpty, keys, keysArray, keysList, lowerBound?, max!, max?, mergeWith, min!, min?, ofArray, ofList, sdiff, single, size, toList, values, valuesArray, valuesList, RBNode, All, Any, Balanced, EMem, Mem, MemP, Ordered, Path, del, erase, fill, ins, insert, insertNew, instDecidableEMem, instDecidableMem, instDecidableMemP, instDecidableOrdered, foldl, foldr, next?, toList, all, all₂, alter, any, append, balLeft, balRight, balance1, balance2, cmpEq, cmpLT, del, erase, find?, fold, foldl, foldlM, foldr, forIn, visit, forM, ins, insert, instBEq, instDecidableAllOfDecidablePred, instDecidableAnyOfDecidablePred, instDecidableCmpEqOfTransCmp, instDecidableCmpLTOfTransCmp, instEmptyCollection, instForInOfMonad, instMembership, instStreamStream, instToStreamStream, isBlack, isOrdered, isRed, lowerBound?, map, max?, min?, modify, reverse, root?, setBlack, setRed, size, toArray, toList, toStream, upperBound?, zoom, RBSet, AlterWF, EMem, Mem, MemP, ModifyWF, instDecidableEMem, instDecidableMem, instDecidableMemP, all, all₂, alterP, any, contains, containsP, empty, erase, filter, find!, find?, findP!, findP?, findPD, foldl, foldlM, foldr, forM, insert, insertMany, instBEq, instEmptyCollection, instForInOfMonad, instInhabited, instMembership, instRepr, instSDiff, instToStreamStream, instUnion, intersectWith, isEmpty, lowerBound?, lowerBoundP?, map, max!, max?, mergeWith, min!, min?, modifyP, ofArray, ofList, sdiff, single, size, toList, union, upperBound?, upperBoundP?, instEmptyCollectionRBMap, instInhabitedRBMap, instReprRBColor, repr, instReprRBNode, repr, mkRBMap, mkRBSet, toRBMap | 205 |
Theoremsimp, all_iff, any_iff, cmpEq_iff, cmpLT_iff, wf, wf | 7 |
| Total | 212 |
| Name | Category | Theorems |
|---|
Keys 📖 | CompOp | — |
Values 📖 | CompOp | — |
all 📖 | CompOp | — |
all₂ 📖 | CompOp | — |
any 📖 | CompOp | — |
contains 📖 | CompOp | 2 bridgebridge: contains_iff_findEntry?, contains_iff_find?
|
empty 📖 | CompOp | 1 mathmath: empty_eq
|
eqKeys 📖 | CompOp | — |
erase 📖 | CompOp | — |
filter 📖 | CompOp | — |
find! 📖 | CompOp | — |
find? 📖 | CompOp | 5 math, 1 bridgemath: find?_congr, find?_some, find?_insert, find?_insert_of_eq, find?_insert_of_ne
bridge: contains_iff_find?
|
findD 📖 | CompOp | — |
findEntry? 📖 | CompOp | 5 math, 1 bridgemath: findEntry?_insert, findEntry?_some, findEntry?_insert_of_eq, findEntry?_insert_of_ne, findEntry?_congr
bridge: contains_iff_findEntry?
|
foldl 📖 | CompOp | 1 mathmath: foldl_eq_foldl_toList
|
foldlM 📖 | CompOp | 1 mathmath: foldlM_eq_foldlM_toList
|
foldr 📖 | CompOp | 1 mathmath: foldr_eq_foldr_toList
|
forM 📖 | CompOp | 1 mathmath: forM_eq_forM_toList
|
insert 📖 | CompOp | 9 mathmath: mem_toList_insert_of_mem, findEntry?_insert, mem_toList_insert_self, mem_toList_insert, find?_insert, findEntry?_insert_of_eq, findEntry?_insert_of_ne, find?_insert_of_eq, find?_insert_of_ne
|
instBEq 📖 | CompOp | — |
instCoeHeadKeysArray 📖 | CompOp | — |
instCoeHeadKeysList 📖 | CompOp | — |
instCoeHeadValuesArray 📖 | CompOp | — |
instCoeHeadValuesList 📖 | CompOp | — |
instForInKeysOfMonad 📖 | CompOp | — |
instForInProdOfMonad 📖 | CompOp | 1 mathmath: forIn_eq_forIn_toList
|
instForInValuesOfMonad 📖 | CompOp | — |
instForMKeysOfMonad 📖 | CompOp | — |
instForMValuesOfMonad 📖 | CompOp | — |
instRepr 📖 | CompOp | — |
instStreamStream 📖 | CompOp | — |
instStreamStream_1 📖 | CompOp | — |
instToStreamKeysStream 📖 | CompOp | — |
instToStreamStreamProd 📖 | CompOp | 2 mathmath: toStream_toList, toStream_eq
|
instToStreamValuesStream 📖 | CompOp | — |
intersectWith 📖 | CompOp | — |
isEmpty 📖 | CompOp | — |
keys 📖 | CompOp | — |
keysArray 📖 | CompOp | — |
keysList 📖 | CompOp | — |
lowerBound? 📖 | CompOp | — |
max! 📖 | CompOp | — |
max? 📖 | CompOp | — |
mergeWith 📖 | CompOp | — |
min! 📖 | CompOp | — |
min? 📖 | CompOp | — |
ofArray 📖 | CompOp | — |
ofList 📖 | CompOp | — |
sdiff 📖 | CompOp | — |
single 📖 | CompOp | 1 mathmath: single_toList
|
size 📖 | CompOp | 1 mathmath: size_eq
|
toList 📖 | CompOp | 18 mathmath: forIn_eq_forIn_toList, toList_sorted, single_toList, toStream_toList, findEntry?_some_mem_toList, findEntry?_some, find?_some, foldr_eq_foldr_toList, find?_some_mem_toList, foldlM_eq_foldlM_toList, mem_toList_insert_self, foldl_eq_foldl_toList, mem_toList_insert, empty_toList, forM_eq_forM_toList, mem_toList, size_eq, val_toList
|
values 📖 | CompOp | — |
valuesArray 📖 | CompOp | — |
valuesList 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
All 📖 | MathDef | 8 math, 2 bridgemath: Path.Ordered.fill, All_and, balance2_All, balance1_All, All.trivial, Ordered.zoom, All.reverse, All_def
bridge: isOrdered_iff', all_iff
|
Any 📖 | MathDef | 2 math, 1 bridgemath: Any_reverse, Any_def
bridge: any_iff
|
Balanced 📖 | CompData | 8 mathmath: WF.out, Path.Balanced.ins, RedRed.setBlack, Path.Balanced.del, RedRed.of_false, WF_iff, RedRed.of_red, Path.Balanced.insertNew
|
EMem 📖 | MathDef | — |
Mem 📖 | MathDef | 3 mathmath: mem_def, Mem_reverse, mem_congr
|
MemP 📖 | MathDef | 6 mathmath: Ordered.memP_iff_lowerBound?, Ordered.memP_iff_find?, memP_def, Ordered.memP_iff_upperBound?, find?_some_memP, memP_reverse
|
Ordered 📖 | MathDef | 7 math, 2 bridgemath: WF.out, Path.Ordered.fill, ordered_iff, WF_iff, Path.Ordered.insertNew, Ordered.setRed, Ordered.setBlack
bridge: isOrdered_iff', isOrdered_iff
|
Path 📖 | CompData | 1 mathmath: find?_eq_zoom
|
all 📖 | CompOp | 1 bridgebridge: all_iff
|
all₂ 📖 | CompOp | — |
alter 📖 | CompOp | 5 mathmath: WF.alter, Batteries.RBSet.AlterWF.wf, modify_eq_alter, Ordered.alter, Balanced.alter
|
any 📖 | CompOp | 1 bridgebridge: any_iff
|
append 📖 | CompOp | 3 mathmath: Ordered.append, Balanced.append, All.append
|
balLeft 📖 | CompOp | 6 mathmath: Ordered.balLeft, reverse_balLeft, Balanced.balLeft, All.balLeft, reverse_balRight, balLeft_toList
|
balRight 📖 | CompOp | 6 mathmath: reverse_balLeft, reverse_balRight, balRight_toList, Ordered.balRight, Balanced.balRight, All.balRight
|
balance1 📖 | CompOp | 7 mathmath: balance1_eq, reverse_balance1, balance1_All, RedRed.balance1, reverse_balance2, balance1_toList, Ordered.balance1
|
balance2 📖 | CompOp | 7 mathmath: balance2_All, Ordered.balance2, reverse_balance1, balance2_eq, balance2_toList, reverse_balance2, RedRed.balance2
|
cmpEq 📖 | MathDef | 1 mathmath: cmpEq_iff
|
cmpLT 📖 | MathDef | 12 math, 1 bridgemath: Batteries.RBMap.toList_sorted, cmpEq.lt_congr_right, ordered_iff, cmpEq.lt_congr_left, Batteries.RBSet.toList_sorted, cmpLT.trans, Path.rootOrdered_iff, cmpLT.flip, Path.ordered_iff, IsMonotone.lt_mono, cmpLT_iff, Ordered.toList_sorted
bridge: isOrdered_iff'
|
del 📖 | CompOp | 4 mathmath: All.del, Balanced.del, Path.zoom_del, Ordered.del
|
erase 📖 | CompOp | 2 mathmath: Balanced.erase, Ordered.erase
|
find? 📖 | CompOp | 6 mathmath: exists_find?_insert_self, find?_eq_zoom, Ordered.memP_iff_find?, find?_insert_self, find?_reverse, Ordered.find?_some
|
fold 📖 | CompOp | — |
foldl 📖 | CompOp | 3 mathmath: foldr_reverse, foldl_reverse, foldl_eq_foldl_toList
|
foldlM 📖 | CompOp | 1 mathmath: foldlM_eq_foldlM_toList
|
foldr 📖 | CompOp | 4 mathmath: foldr_eq_foldr_toList, foldr_reverse, foldl_reverse, foldr_cons
|
forIn 📖 | CompOp | — |
forM 📖 | CompOp | 1 mathmath: forM_eq_forM_toList
|
ins 📖 | CompOp | 6 mathmath: Path.zoom_ins, All.ins, Ordered.ins, Balanced.ins, reverse_ins, insert_setBlack
|
insert 📖 | CompOp | 16 mathmath: mem_insert, exists_find?_insert_self, exists_insert_toList_zoom_node, Ordered.insert, find?_insert_self, insert_toList_zoom, Path.zoom_insert, insert_toList_zoom_nil, Path.insertNew_eq_insert, reverse_insert, Balanced.insert, mem_insert_of_mem, mem_insert_self, insert_toList_zoom_node, exists_insert_toList_zoom_nil, insert_setBlack
|
instBEq 📖 | CompOp | — |
instDecidableAllOfDecidablePred 📖 | CompOp | — |
instDecidableAnyOfDecidablePred 📖 | CompOp | — |
instDecidableCmpEqOfTransCmp 📖 | CompOp | — |
instDecidableCmpLTOfTransCmp 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
instForInOfMonad 📖 | CompOp | 2 mathmath: forIn_eq_forIn_toList, Stream.forIn_eq_forIn_toList
|
instMembership 📖 | CompOp | 21 mathmath: mem_reverse, mem_insert, mem_toList, Ordered.upperBound?_exists, memP_def, max?_mem, mem_def, Any_def, mem_node, Batteries.RBSet.mem_toList, min?_mem, mem_nil, find?_some_mem, lowerBound?_mem_lb, lowerBound?_mem, upperBound?_mem, Ordered.lowerBound?_exists, mem_insert_self, upperBound?_mem_ub, Batteries.RBMap.mem_toList, Ordered.find?_some
|
instStreamStream 📖 | CompOp | — |
instToStreamStream 📖 | CompOp | — |
isBlack 📖 | CompOp | 1 mathmath: Balanced.del
|
isOrdered 📖 | CompOp | 2 bridgebridge: isOrdered_iff', isOrdered_iff
|
isRed 📖 | CompOp | 2 mathmath: isRed_reverse, Balanced.ins
|
lowerBound? 📖 | CompOp | 6 mathmath: Ordered.memP_iff_lowerBound?, lowerBound?_of_some, lowerBound?_reverse, lowerBound?_eq_find?, Ordered.lowerBound?_exists, upperBound?_reverse
|
map 📖 | CompOp | 3 mathmath: Ordered.map, All.map, Balanced.map
|
max? 📖 | CompOp | 3 mathmath: max?_reverse, max?_eq_toList_getLast?, min?_reverse
|
min? 📖 | CompOp | 3 mathmath: min?_eq_toList_head?, max?_reverse, min?_reverse
|
modify 📖 | CompOp | 5 mathmath: modify_eq_alter, WF.modify, Batteries.RBSet.ModifyWF.wf, Balanced.modify, Ordered.modify
|
reverse 📖 | CompOp | 28 mathmath: mem_reverse, reverse_balLeft, Ordered.reverse, RedRed.reverse, Balanced.reverse, reverse_setRed, reverse_balance1, Any_reverse, lowerBound?_reverse, foldr_reverse, toList_reverse, reverse_eq_iff, reverse_balRight, Mem_reverse, reverse_size, max?_reverse, reverse_setBlack, foldl_reverse, reverse_reverse, memP_reverse, reverse_insert, isRed_reverse, reverse_balance2, All.reverse, find?_reverse, upperBound?_reverse, reverse_ins, min?_reverse
|
root? 📖 | CompOp | 1 mathmath: find?_eq_zoom
|
setBlack 📖 | CompOp | 10 mathmath: RedRed.setBlack, Balanced.setBlack, setBlack_idem, Path.zoom_insert, reverse_setBlack, setBlack_toList, Path.insertNew_eq_insert, Path.ins_eq_fill, Ordered.setBlack, insert_setBlack
|
setRed 📖 | CompOp | 4 mathmath: reverse_setRed, Ordered.setRed, setRed_toList, All.setRed
|
size 📖 | CompOp | 6 mathmath: WF.depth_bound, size_eq, reverse_size, Balanced.le_size, size_lt_depth, Balanced.depth_bound
|
toArray 📖 | CompOp | — |
toList 📖 | CompOp | 38 mathmath: exists_insert_toList_zoom_node, toStream_toList', mem_toList, ordered_iff, Path.fill_toList, Path.insertNew_toList, zoom_toList, foldr_eq_foldr_toList, forM_eq_forM_toList, size_eq, toList_nil, toList_reverse, toList_node, min?_eq_toList_head?, insert_toList_zoom, forIn_eq_forIn_toList, balance2_toList, setBlack_toList, Batteries.RBSet.val_toList, setRed_toList, toStream_toList, max?_eq_toList_getLast?, foldr_cons, Path.ins_toList, balRight_toList, insert_toList_zoom_nil, forIn_visit_eq_bindList, balLeft_toList, foldl_eq_foldl_toList, Stream.toList_cons, Path.insert_toList, Stream.forIn_eq_forIn_toList, insert_toList_zoom_node, foldlM_eq_foldlM_toList, balance1_toList, exists_insert_toList_zoom_nil, Ordered.toList_sorted, Batteries.RBMap.val_toList
|
toStream 📖 | CompOp | 4 mathmath: toStream_toList', Batteries.RBSet.toStream_eq, Batteries.RBMap.toStream_eq, toStream_toList
|
upperBound? 📖 | CompOp | 6 mathmath: upperBound?_eq_find?, Ordered.upperBound?_exists, Ordered.memP_iff_upperBound?, lowerBound?_reverse, upperBound?_of_some, upperBound?_reverse
|
zoom 📖 | CompOp | 2 mathmath: find?_eq_zoom, Path.zoom_fill'
|
| Name | Category | Theorems |
|---|
AlterWF 📖 | CompData | — |
EMem 📖 | MathDef | — |
Mem 📖 | MathDef | — |
MemP 📖 | MathDef | 4 mathmath: findP?_some_memP, memP_iff_upperBoundP?, memP_iff_findP?, memP_iff_lowerBoundP?
|
ModifyWF 📖 | CompData | 1 mathmath: ModifyWF.of_eq
|
all 📖 | CompOp | — |
all₂ 📖 | CompOp | — |
alterP 📖 | CompOp | — |
any 📖 | CompOp | — |
contains 📖 | CompOp | 1 bridgebridge: contains_iff
|
containsP 📖 | CompOp | — |
empty 📖 | CompOp | 1 mathmath: empty_eq
|
erase 📖 | CompOp | — |
filter 📖 | CompOp | — |
find! 📖 | CompOp | — |
find? 📖 | CompOp | 6 mathmath: find?_insert, find?_congr, find?_some, mem_iff_find?, find?_insert_of_ne, find?_insert_of_eq
|
findP! 📖 | CompOp | — |
findP? 📖 | CompOp | 5 mathmath: findP?_some, findP?_insert_of_ne, findP?_insert, memP_iff_findP?, findP?_insert_of_eq
|
findPD 📖 | CompOp | — |
foldl 📖 | CompOp | 1 mathmath: foldl_eq_foldl_toList
|
foldlM 📖 | CompOp | 1 mathmath: foldlM_eq_foldlM_toList
|
foldr 📖 | CompOp | 1 mathmath: foldr_eq_foldr_toList
|
forM 📖 | CompOp | 1 mathmath: forM_eq_forM_toList
|
insert 📖 | CompOp | 14 mathmath: find?_insert, find?_insert_of_ne, mem_insert_of_mem_toList, mem_insert_of_eq, find?_insert_of_eq, mem_toList_insert_of_mem, findP?_insert_of_ne, mem_toList_insert, findP?_insert, mem_insert_of_mem, mem_toList_insert_self, findP?_insert_of_eq, mem_insert_self, mem_insert
|
insertMany 📖 | CompOp | — |
instBEq 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | 4 mathmath: empty_toList, default_eq, mkRBSet_eq, empty_eq
|
instForInOfMonad 📖 | CompOp | 1 mathmath: forIn_eq_forIn_toList
|
instInhabited 📖 | CompOp | 1 mathmath: default_eq
|
instMembership 📖 | CompOp | 19 math, 1 bridgemath: mem_congr, lowerBoundP?_exists, lowerBound?_mem, mem_iff_find?, lowerBound?_exists, mem_insert_of_mem_toList, mem_insert_of_eq, mem_iff_upperBound?, mem_iff_lowerBound?, mem_of_mem_toList, find?_some_mem, lowerBoundP?_mem, upperBoundP?_exists, upperBound?_exists, upperBoundP?_mem, mem_insert_self, mem_insert, upperBound?_mem, mem_iff_mem_toList
bridge: contains_iff
|
instRepr 📖 | CompOp | — |
instSDiff 📖 | CompOp | — |
instToStreamStream 📖 | CompOp | 2 mathmath: toStream_eq, toStream_toList
|
instUnion 📖 | CompOp | — |
intersectWith 📖 | CompOp | — |
isEmpty 📖 | CompOp | 1 bridgebridge: isEmpty_iff_toList_eq_nil
|
lowerBound? 📖 | CompOp | 3 mathmath: lowerBound?_exists, mem_iff_lowerBound?, lowerBound?_eq_find?
|
lowerBoundP? 📖 | CompOp | 3 mathmath: lowerBoundP?_exists, lowerBoundP?_eq_findP?, memP_iff_lowerBoundP?
|
map 📖 | CompOp | — |
max! 📖 | CompOp | — |
max? 📖 | CompOp | — |
mergeWith 📖 | CompOp | — |
min! 📖 | CompOp | — |
min? 📖 | CompOp | — |
modifyP 📖 | CompOp | — |
ofArray 📖 | CompOp | — |
ofList 📖 | CompOp | — |
sdiff 📖 | CompOp | — |
single 📖 | CompOp | 1 mathmath: single_toList
|
size 📖 | CompOp | 1 mathmath: size_eq
|
toList 📖 | CompOp | 23 math, 1 bridgemath: findP?_some_mem_toList, empty_toList, single_toList, find?_some, size_eq, find?_some_mem_toList, upperBound?_mem_toList, toList_sorted, lowerBound?_mem_toList, toStream_toList, mem_toList, val_toList, findP?_some, foldl_eq_foldl_toList, forM_eq_forM_toList, lowerBoundP?_mem_toList, mem_toList_insert, foldr_eq_foldr_toList, mem_toList_insert_self, foldlM_eq_foldlM_toList, forIn_eq_forIn_toList, upperBoundP?_mem_toList, mem_iff_mem_toList
bridge: isEmpty_iff_toList_eq_nil
|
union 📖 | CompOp | — |
upperBound? 📖 | CompOp | 3 mathmath: upperBound?_eq_find?, mem_iff_upperBound?, upperBound?_exists
|
upperBoundP? 📖 | CompOp | 3 mathmath: upperBoundP?_eq_findP?, memP_iff_upperBoundP?, upperBoundP?_exists
|