| Metric | Count |
|---|
DefinitionsOrdnode, All, decidable, Amem, decidable, Any, decidable, Emem, decidable, adjustWith, alter, attach', balance, balanceL, balanceR, copair, delta, diff, disjoint, drop, dropAux, dropWhile, dual, empty, erase, eraseMax, eraseMin, filter, find, findGe, findGeAux, findGt, findGtAux, findIndex, findIndexAux, findLe, findLeAux, findLt, findLtAux, findMax, findMax', findMin, findMin', fold, foldl, foldr, glue, image, insert, insert', insertMax, insertMin, insertWith, instDecidableRelEquivOfDecidableEq, instEmptyCollection, instInhabited, instInsert, instMembership, instRepr, instSingleton, instToFormat, instToString, inter, isSubset, isSubsetAux, link, map, mem, decidable, merge, node', nth, ofAscList, ofAscListAux₁, ofAscListAux₂, ofList, ofList', partition, pmap, powerset, prod, ratio, removeNth, repr, singleton, size, span, split, split3, splitAt, splitAtAux, splitMax, splitMax', splitMin, splitMin', take, takeAux, takeWhile, toList, toRevList, union, updateWith | 102 |
Theoremssize_nil, size_node | 2 |
| Total | 104 |
| Name | Category | Theorems |
|---|
All 📖 | MathDef | 16 mathmath: Bounded.to_sep, all_node4R, all_dual, all_node3R, all_singleton, all_node4L, all_node', all_rotateL, all_balance', all_iff_forall, all_rotateR, all_node3L, all_balanceL, all_balanceR, Bounded.mem_gt, Bounded.mem_lt
|
Amem 📖 | MathDef | — |
Any 📖 | MathDef | 2 mathmath: any_singleton, any_iff_exists
|
Emem 📖 | MathDef | 3 mathmath: any_iff_exists, emem_iff_mem_toList, emem_iff_all
|
adjustWith 📖 | CompOp | — |
alter 📖 | CompOp | — |
attach' 📖 | CompOp | — |
balance 📖 | CompOp | 3 mathmath: balance_eq_balance', balanceL_eq_balance, Valid'.balance
|
balanceL 📖 | CompOp | 10 mathmath: Valid'.balanceL, balanceL_eq_balance', dual_balanceL, size_balanceL, balanceL_eq_balance, merge_node, dual_balanceR, Valid'.merge_aux₁, Valid'.balanceL_aux, all_balanceL
|
balanceR 📖 | CompOp | 8 mathmath: dual_balanceL, Valid'.balanceR_aux, merge_node, size_balanceR, dual_balanceR, balanceR_eq_balance', Valid'.balanceR, all_balanceR
|
copair 📖 | CompOp | — |
delta 📖 | CompOp | 2 mathmath: merge_node, not_le_delta
|
diff 📖 | CompOp | — |
disjoint 📖 | CompOp | — |
drop 📖 | CompOp | — |
dropAux 📖 | CompOp | — |
dropWhile 📖 | CompOp | — |
dual 📖 | CompOp | 30 mathmath: Valid.dual_iff, balance_sz_dual, dual_node', Sized.dual_iff, dual_balanceL, dual_eraseMax, Bounded.dual, all_dual, Valid.dual, size_dual, dual_eraseMin, dual_node4L, dual_node3L, dual_balanceR, dual_rotateR, dual_node4R, findMax'_dual, Balanced.dual, findMin_dual, dual_rotateL, dual_balance', findMin'_dual, dual_node3R, findMax_dual, dual_insert, Sized.dual, Valid'.dual, Bounded.dual_iff, Valid'.dual_iff, dual_dual
|
empty 📖 | CompOp | 1 bridgebridge: Ordset.empty_iff
|
erase 📖 | CompOp | 3 mathmath: erase.valid, size_erase_of_mem, Valid'.erase_aux
|
eraseMax 📖 | CompOp | 5 mathmath: dual_eraseMax, eraseMax.valid, dual_eraseMin, splitMax_eq, Valid'.eraseMax_aux
|
eraseMin 📖 | CompOp | 5 mathmath: eraseMin.valid, dual_eraseMax, dual_eraseMin, splitMin_eq, Valid'.eraseMin_aux
|
filter 📖 | CompOp | — |
find 📖 | CompOp | — |
findGe 📖 | CompOp | — |
findGeAux 📖 | CompOp | — |
findGt 📖 | CompOp | — |
findGtAux 📖 | CompOp | — |
findIndex 📖 | CompOp | — |
findIndexAux 📖 | CompOp | — |
findLe 📖 | CompOp | — |
findLeAux 📖 | CompOp | — |
findLt 📖 | CompOp | — |
findLtAux 📖 | CompOp | — |
findMax 📖 | CompOp | 2 mathmath: findMin_dual, findMax_dual
|
findMax' 📖 | CompOp | 5 mathmath: findMax'_all, splitMax_eq, findMax'_dual, findMin'_dual, Valid'.eraseMax_aux
|
findMin 📖 | CompOp | 2 mathmath: findMin_dual, findMax_dual
|
findMin' 📖 | CompOp | 5 mathmath: splitMin_eq, findMax'_dual, Valid'.eraseMin_aux, findMin'_dual, findMin'_all
|
fold 📖 | CompOp | — |
foldl 📖 | CompOp | — |
foldr 📖 | CompOp | 1 mathmath: foldr_cons_eq_toList
|
glue 📖 | CompOp | 3 mathmath: Valid'.glue_aux, merge_node, Valid'.glue
|
image 📖 | CompOp | — |
insert 📖 | CompOp | 3 mathmath: dual_insert, insert_eq_insertWith, insert.valid
|
insert' 📖 | CompOp | 2 mathmath: insert'_eq_insertWith, insert'.valid
|
insertMax 📖 | CompOp | — |
insertMin 📖 | CompOp | — |
insertWith 📖 | CompOp | 4 mathmath: insertWith.valid, insert'_eq_insertWith, insertWith.valid_aux, insert_eq_insertWith
|
instDecidableRelEquivOfDecidableEq 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instInsert 📖 | CompOp | — |
instMembership 📖 | CompOp | — |
instRepr 📖 | CompOp | — |
instSingleton 📖 | CompOp | 4 mathmath: any_singleton, all_singleton, valid_singleton, valid'_singleton
|
instToFormat 📖 | CompOp | — |
instToString 📖 | CompOp | — |
inter 📖 | CompOp | — |
isSubset 📖 | CompOp | — |
isSubsetAux 📖 | CompOp | — |
link 📖 | CompOp | — |
map 📖 | CompOp | 2 mathmath: map.valid, Valid'.map_aux
|
mem 📖 | CompOp | — |
merge 📖 | CompOp | 5 mathmath: merge_nil_right, merge_nil_left, Valid.merge, merge_node, Valid'.merge_aux
|
node' 📖 | CompOp | 10 mathmath: dual_node', Sized.eq_node', all_node', Sized.node', Valid'.eraseMin_aux, rotateR_nil, Valid'.node', Raised.right, rotateL_nil, Valid'.eraseMax_aux
|
nth 📖 | CompOp | — |
ofAscList 📖 | CompOp | — |
ofAscListAux₁ 📖 | CompOp | — |
ofAscListAux₂ 📖 | CompOp | — |
ofList 📖 | CompOp | — |
ofList' 📖 | CompOp | — |
partition 📖 | CompOp | — |
pmap 📖 | CompOp | — |
powerset 📖 | CompOp | — |
prod 📖 | CompOp | — |
ratio 📖 | CompOp | 2 mathmath: rotateL_node, rotateR_node
|
removeNth 📖 | CompOp | — |
repr 📖 | CompOp | — |
singleton 📖 | CompOp | — |
size 📖 | CompOp | 24 mathmath: node4L_size, size_node, node3R_size, size_eq_realSize, size_nil, Sized.size_eq_zero, pos_size_of_mem, size_dual, Sized.rotateL_size, length_toList, Valid'.map_aux, insertWith.valid_aux, size_erase_of_mem, Sized.rotateR_size, Valid'.eraseMin_aux, size_balance', Valid'.merge_aux, rotateL_node, Valid'.erase_aux, rotateR_node, node3L_size, Valid.size_eq, Sized.size_eq, Valid'.eraseMax_aux
|
span 📖 | CompOp | — |
split 📖 | CompOp | — |
split3 📖 | CompOp | — |
splitAt 📖 | CompOp | — |
splitAtAux 📖 | CompOp | — |
splitMax 📖 | CompOp | — |
splitMax' 📖 | CompOp | 1 mathmath: splitMax_eq
|
splitMin 📖 | CompOp | — |
splitMin' 📖 | CompOp | 1 mathmath: splitMin_eq
|
take 📖 | CompOp | — |
takeAux 📖 | CompOp | — |
takeWhile 📖 | CompOp | — |
toList 📖 | CompOp | 7 mathmath: toList_nil, foldr_cons_eq_toList, toList_node, length_toList, equiv_iff, emem_iff_mem_toList, length_toList'
|
toRevList 📖 | CompOp | — |
union 📖 | CompOp | — |
updateWith 📖 | CompOp | — |