batteries
batteries copied to clipboard
leanprover-community
The "batteries included" extended library for the Lean programming language and theorem prover
In reviewing documentation examples for HashMap, @digama0 [mentioned that it would be nice to have syntax for constructing concrete HashMaps](https://github.com/leanprover/std4/pull/725#discussion_r1558731044). The proposed syntax is `{"one" ↦ 2, "two" ↦ 2}`...
This adds a function `Buckets.toListModel`. It models an array of buckets as a list of (key, value) pairs. We prove a number of lemmas about the behaviour of this model...
Some of the definitions have been modified to be faster. - [x] depends on: #464 - [x] depends on: #465
Unfortunately `Fin.last` doesn't allow you to talk about the top element of `Fin (2^n)`. This fills that gap. Not certain it is a good idea.
Ordered wrapper around `AssocList`, and basic functions `find?`, `insert?`, `filterMapVal`, and `merge`. An extensionality lemma `(∀ a, l₁.find? a = l₂.find? a) → l₁ = l₂`. I will later use...
This changes the way the pattern for `change` is elaborated so that it's able to assign to synthetic opaque metavariables in a controlled way. This allows the following Lean 3...
This is upstreaming the function from Mathlib.
This uses the associativity, commutativity and identity classes recently added to Lean core to define folds with simplification lemmas that can move intermediate results outside the fold for better use...
Metadata
Owner
Metadata
The "batteries included" extended library for the Lean programming language and theorem prover