Theorems · Inductive type
AList
{α : Type u} → (α → Type v) → Type (max u v)AList β is a key-value map stored as a List (i.e. a linked list).
It is a wrapper around certain List functions with the added constraint
that the list have unique keys.
- Defined in
- Mathlib.Data.List.AList
- Cited by
- 122 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by152
Results whose statement or proof uses this declaration.
- AList.entriesstatement and proof · cited by 44
- AList.toFinmapstatement and proof · cited by 33
- AList.lookupstatement and proof · cited by 28
- Finmap.lookupproof · cited by 28
- AList.insertstatement and proof · cited by 27
- Finmap.induction_onstatement and proof · cited by 22
- AList.nodupKeysstatement and proof · cited by 15
- AList.keysstatement and proof · cited by 13
- AList.erasestatement and proof · cited by 12
- Finmap.induction_on₂statement and proof · cited by 10
- Finmap.insertproof · cited by 10
- AList.extstatement and proof · cited by 9