AList.nodupKeys
theorem AList.nodupKeys : ∀ {α : Type u} {β : α → Type v} (self : AList β), self.entries.NodupKeys
This theorem, `AList.nodupKeys`, asserts that in an Association List (`AList`), there are no duplicate keys. An `AList` is a type of list where each element is a key-value pair, and the type of value is dependent on the key. The `nodupKeys` property guarantees that each key is unique within the list, meaning each key appears only once in the list's entries. This theorem holds for any `AList` and any types of keys (`α`) and associated values (`β`).
More concisely: In an Association List (AList) of key-value pairs (α × β), each key α appears only once.
|
AList.lookup_isSome
theorem AList.lookup_isSome :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : AList β},
(AList.lookup a s).isSome = true ↔ a ∈ s
This theorem states that for any type `α`, any type `β` that depends on `α`, any instance of decidable equality on `α`, and any key-value pair `a` and `s` of type `α` and `AList β` respectively, the function `Option.isSome` applied to the result of looking up `a` in `s` is `true` if and only if `a` is an element of `s`. In other words, it establishes a correspondence between the successful lookup of an element in an association list and the presence of that element in the list.
More concisely: For any type `α`, any type `β`, and any association list `s : AList β` of pairs between type `α` and type `β`, the option type `Option.isSome (s.find ?a)` is equal to `true` if and only if `a` is an element of `s`.
|
AList.mem_keys
theorem AList.mem_keys : ∀ {α : Type u} {β : α → Type v} {a : α} {s : AList β}, a ∈ s ↔ a ∈ s.keys
This theorem, `AList.mem_keys`, states that for any type `α`, for any dependent type `β` that depends on `α`, for any value `a` of type `α`, and for any association list `s` of type `β`, `a` is in the list `s` if and only if `a` is in the list of keys of `s`. In other words, it states that an element belongs to an association list if and only if it is a key in that association list.
More concisely: For any type `α` and dependent type `β`, an element `a` of type `α` is in an association list `s` of type `β` if and only if `a` is a key in `s`.
|
AList.ext
theorem AList.ext : ∀ {α : Type u} {β : α → Type v} {s t : AList β}, s.entries = t.entries → s = t
This is a theorem about associative lists (ALists) in the Lean 4 theorem prover. It states that for any type `α` and a type function `β` that depends on `α`, given two associative lists `s` and `t` with the type of keys determined by `α` and the type of values determined by `β`, if the entries of `s` and `t` are equal (that is, they have the same key-value pairs in the same order), then the associative lists `s` and `t` themselves are equal. This is a fundamental property of data structures like associative lists, which essentially states that two associative lists are equal if they have the same content.
More concisely: If two associative lists of type `α × β` have equal entries, then they are equal as lists.
|