batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Add HashMap model

Open Vtec234 opened this issue 2 years ago • 1 comments

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 w.r.t. various map operations. No further propositions are proven in this PR, in particular it doesn't add any facts about the relations between user-facing HashMap operations just yet.

Depends on #89 and #272. See #38 for previous attempt.

Vtec234 avatar Oct 05 '23 04:10 Vtec234

Could we split this up? I'd happily merge the Std/Data/List part immediately, and that then makes the rest easier.

kim-em avatar Mar 26 '24 22:03 kim-em