AssocList

📁 Source: Batteries/Data/AssocList.lean

Statistics

Metric	Count
Definitions `AssocList`, `All`, `all`, `any`, `beq`, `contains`, `erase`, `eraseP`, `find?`, `findEntry?`, `findEntryP?`, `foldl`, `foldlM`, `forIn`, `forM`, `instBEq`, `instEmptyCollection`, `instForInProdOfMonad`, `instStreamProd`, `instToStream`, `isEmpty`, `length`, `mapKey`, `mapVal`, `modify`, `pop?`, `replace`, `toList`, `toListTR`, `instInhabitedAssocList`, `default`, `toAssocList`	32
Theorems `all_eq`, `any_eq`, `beq_cons_nil`, `beq_cons₂`, `beq_eq`, `beq_nil_cons`, `beq_nil₂`, `contains_eq`, `empty_eq`, `find?_eq`, `find?_eq_findEntry?`, `findEntry?_eq`, `findEntryP?_eq`, `foldlM_eq`, `foldl_eq`, `forIn_eq`, `forM_eq`, `instLawfulBEq`, `isEmpty_eq`, `length_cons`, `length_mapKey`, `length_mapVal`, `length_modify`, `length_nil`, `length_replace`, `length_toList`, `toList_eq_toListTR`, `toList_erase`, `toList_eraseP`, `toList_mapKey`, `toList_mapVal`, `toList_modify`, `toList_replace`, `toList_toAssocList`, `length_toAssocList`, `toList_toAssocList`	36
Total	68

Batteries

Definitions

Name	Category	Theorems
`AssocList` 📖	CompData	8 math math: `AssocList.beq_nil_cons`, `AssocList.beq_cons₂`, `AssocList.beq_cons_nil`, `AssocList.beq_nil₂`, `AssocList.beq_eq`, `AssocList.instLawfulBEq`, `AssocList.forIn_eq`, `AssocList.empty_eq`
`instInhabitedAssocList` 📖	CompOp	—

Batteries.AssocList

Definitions

Name	Category	Theorems
`All` 📖	MathDef	—
`all` 📖	CompOp	1 math math: `all_eq`
`any` 📖	CompOp	1 math math: `any_eq`
`beq` 📖	CompOp	—
`contains` 📖	CompOp	1 math math: `contains_eq`
`erase` 📖	CompOp	1 math math: `toList_erase`
`eraseP` 📖	CompOp	1 math math: `toList_eraseP`
`find?` 📖	CompOp	2 math math: `find?_eq_findEntry?`, `find?_eq`
`findEntry?` 📖	CompOp	2 math math: `find?_eq_findEntry?`, `findEntry?_eq`
`findEntryP?` 📖	CompOp	1 math math: `findEntryP?_eq`
`foldl` 📖	CompOp	1 math math: `foldl_eq`
`foldlM` 📖	CompOp	1 math math: `foldlM_eq`
`forIn` 📖	CompOp	—
`forM` 📖	CompOp	1 math math: `forM_eq`
`instBEq` 📖	CompOp	6 math math: `beq_nil_cons`, `beq_cons₂`, `beq_cons_nil`, `beq_nil₂`, `beq_eq`, `instLawfulBEq`
`instEmptyCollection` 📖	CompOp	1 math math: `empty_eq`
`instForInProdOfMonad` 📖	CompOp	1 math math: `forIn_eq`
`instStreamProd` 📖	CompOp	—
`instToStream` 📖	CompOp	—
`isEmpty` 📖	CompOp	1 math math: `isEmpty_eq`
`length` 📖	CompOp	8 math math: `length_modify`, `length_toList`, `length_mapVal`, `length_replace`, `length_nil`, `List.length_toAssocList`, `length_mapKey`, `length_cons`
`mapKey` 📖	CompOp	2 math math: `length_mapKey`, `toList_mapKey`
`mapVal` 📖	CompOp	2 math math: `length_mapVal`, `toList_mapVal`
`modify` 📖	CompOp	2 math math: `length_modify`, `toList_modify`
`pop?` 📖	CompOp	—
`replace` 📖	CompOp	2 math math: `length_replace`, `toList_replace`
`toList` 📖	CompOp	22 math math: `contains_eq`, `length_toList`, `any_eq`, `List.toList_toAssocList`, `isEmpty_eq`, `foldl_eq`, `toList_erase`, `all_eq`, `toList_mapVal`, `toList_eq_toListTR`, `beq_eq`, `forIn_eq`, `toList_toAssocList`, `foldlM_eq`, `find?_eq`, `toList_modify`, `findEntry?_eq`, `findEntryP?_eq`, `toList_replace`, `toList_eraseP`, `forM_eq`, `toList_mapKey`
`toListTR` 📖	CompOp	1 math math: `toList_eq_toListTR`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`all_eq` 📖	mathematical	—	`all` `toList`	—	—
`any_eq` 📖	mathematical	—	`any` `toList`	—	—
`beq_cons_nil` 📖	mathematical	—	`Batteries.AssocList` `instBEq` `cons` `nil`	—	—
`beq_cons₂` 📖	mathematical	—	`Batteries.AssocList` `instBEq` `cons`	—	—
`beq_eq` 📖	mathematical	—	`Batteries.AssocList` `instBEq` `toList`	—	—
`beq_nil_cons` 📖	mathematical	—	`Batteries.AssocList` `instBEq` `nil` `cons`	—	—
`beq_nil₂` 📖	mathematical	—	`Batteries.AssocList` `instBEq` `nil`	—	—
`contains_eq` 📖	mathematical	—	`contains` `toList`	—	`any_eq`
`empty_eq` 📖	mathematical	—	`Batteries.AssocList` `instEmptyCollection` `nil`	—	—
`find?_eq` 📖	mathematical	—	`find?` `toList`	—	`find?_eq_findEntry?` `findEntry?_eq`
`find?_eq_findEntry?` 📖	mathematical	—	`find?` `findEntry?`	—	`findEntry?_eq`
`findEntry?_eq` 📖	mathematical	—	`findEntry?` `toList`	—	`findEntryP?_eq`
`findEntryP?_eq` 📖	mathematical	—	`findEntryP?` `toList`	—	—
`foldlM_eq` 📖	mathematical	—	`foldlM` `toList`	—	—
`foldl_eq` 📖	mathematical	—	`foldl` `toList`	—	`foldlM_eq`
`forIn_eq` 📖	mathematical	—	`Batteries.AssocList` `instForInProdOfMonad` `toList`	—	—
`forM_eq` 📖	mathematical	—	`forM` `toList`	—	—
`instLawfulBEq` 📖	mathematical	—	`Batteries.AssocList` `instBEq`	—	—
`isEmpty_eq` 📖	mathematical	—	`isEmpty` `toList`	—	—
`length_cons` 📖	mathematical	—	`length` `cons`	—	—
`length_mapKey` 📖	mathematical	—	`length` `mapKey`	—	—
`length_mapVal` 📖	mathematical	—	`length` `mapVal`	—	—
`length_modify` 📖	mathematical	—	`length` `modify`	—	—
`length_nil` 📖	mathematical	—	`length` `nil`	—	—
`length_replace` 📖	mathematical	—	`length` `replace`	—	—
`length_toList` 📖	mathematical	—	`toList` `length`	—	—
`toList_eq_toListTR` 📖	mathematical	—	`toList` `toListTR`	—	`foldl_eq`
`toList_erase` 📖	mathematical	—	`toList` `erase`	—	`toList_eraseP`
`toList_eraseP` 📖	mathematical	—	`toList` `eraseP`	—	—
`toList_mapKey` 📖	mathematical	—	`toList` `mapKey`	—	—
`toList_mapVal` 📖	mathematical	—	`toList` `mapVal`	—	—
`toList_modify` 📖	mathematical	—	`toList` `modify` `List.replaceF`	—	—
`toList_replace` 📖	mathematical	—	`toList` `replace` `List.replaceF`	—	—
`toList_toAssocList` 📖	mathematical	—	`List.toAssocList` `toList`	—	—

Batteries.instInhabitedAssocList

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

List

Definitions

Name	Category	Theorems
`toAssocList` 📖	CompOp	3 math math: `toList_toAssocList`, `length_toAssocList`, `Batteries.AssocList.toList_toAssocList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_toAssocList` 📖	mathematical	—	`Batteries.AssocList.length` `toAssocList`	—	—
`toList_toAssocList` 📖	mathematical	—	`Batteries.AssocList.toList` `toAssocList`	—	—

---

← Back to Index