Code

feat: Std.HashMap#4583

Code

Merged

TwoFX merged 46 commits intomasterleanprover/lean4:masterfrom markus/std-hashmapleanprover/lean4:markus/std-hashmapCopy head branch name to clipboardJul 5, 2024

+9,725-1

Commits

Commits on Jul 4, 2024

• Initial code import

  TwoFX

  committed
  cbee7b1

  Copy full SHA for cbee7b1

• Put everything in prelude

  TwoFX

  committed
  d89818d

  Copy full SHA for d89818d

• Make mkIdx inline and remove unused Nat lemma

  TwoFX

  committed
  d483bc1

  Copy full SHA for d483bc1

• Fix definition incorrectly referring to Raw

  TwoFX

  committed
  525b943

  Copy full SHA for 525b943

• Consistent place for mem_iff_contains

  TwoFX

  committed
  6811261

  Copy full SHA for 6811261

• Split lemmas about Raw into separate files

  TwoFX

  committed
  55ab1a2

  Copy full SHA for 55ab1a2

• Rename lemmas involving structure projections

  TwoFX

  committed
  fb061b6

  Copy full SHA for fb061b6

• Group unverified functions together

  TwoFX

  committed
  d23a40d

  Copy full SHA for d23a40d

• Add Internal.numBuckets

  TwoFX

  committed
  9ba7045

  Copy full SHA for 9ba7045

• Add simple tests for unverified operations

  TwoFX

  committed
  1ca7bb8

  Copy full SHA for 1ca7bb8

• Add Repr instance

  TwoFX

  committed
  04a7cf4

  Copy full SHA for 04a7cf4

• Reverse result order of 'Then' functions

  TwoFX

  committed
  e2c8e70

  Copy full SHA for e2c8e70

• Add docstrings to DHashMap/Basic

  TwoFX

  committed
  741ef8c

  Copy full SHA for 741ef8c

• Separate definitions for DHashMap and DHashMap.Raw

  TwoFX

  committed
  cb777b6

  Copy full SHA for cb777b6

• Separate definitions for HashMap and HashSet

  TwoFX

  committed
  9b86acf

  Copy full SHA for 9b86acf

• Docs in DHashMap/AdditionalOperations.lean

  TwoFX

  committed
  d3000bc

  Copy full SHA for d3000bc

• Docstrings for HashMap and HashSet

  TwoFX

  committed
  102b33b

  Copy full SHA for 102b33b

• Fix test

  TwoFX

  committed
  7622d7b

  Copy full SHA for 7622d7b

• Add HashMap.lean and friends

  TwoFX

  committed
  ef97ffc

  Copy full SHA for ef97ffc

• Redefine HashSet.insert to use HashMap.insertIfNew

  TwoFX

  committed
  29c5134

  Copy full SHA for 29c5134

• Fix

  TwoFX

  committed
  58cd6e4

  Copy full SHA for 58cd6e4

• Rephrase docstrings

  TwoFX

  committed
  75755de

  Copy full SHA for 75755de

• Add simple module docs to internal files

  TwoFX

  committed
  1a8d517

  Copy full SHA for 1a8d517

• Remove some outdated comments in Internal

  TwoFX

  committed
  bfb6672

  Copy full SHA for bfb6672

• Switch to other sigma syntax

  TwoFX

  committed
  acc69ad

  Copy full SHA for acc69ad

• One hundred columns

  TwoFX

  committed
  023d190

  Copy full SHA for 023d190

• Add Std.lean and Data.lean

  TwoFX

  committed
  ed6b42b

  Copy full SHA for ed6b42b

• Apply build fix suggested by Sebastian

  TwoFX

  committed
  27fd0ac

  Copy full SHA for 27fd0ac

• Drop Std/Classes and Std/Init

  TwoFX

  committed
  20ed6ef

  Copy full SHA for 20ed6ef

Commits on Jul 5, 2024

• Switch to preferred style for multiline comments

  TwoFX

  committed
  c713565

  Copy full SHA for c713565

• Improve docstrings for (D)HashMap(.Raw)

  TwoFX

  committed
  8f13d94

  Copy full SHA for 8f13d94

• Expand docstrings for Then operations and use indicative mood

  TwoFX

  committed
  cc52e78

  Copy full SHA for cc52e78

• More docstring fixes then Then operations

  TwoFX

  committed
  7ffd770

  Copy full SHA for 7ffd770

• foldl -> fold

  TwoFX

  committed
  f204cf0

  Copy full SHA for f204cf0

• Improve docstring for forM

  TwoFX

  committed
  9189112

  Copy full SHA for 9189112

• Clarify naming of WF lemmas

  TwoFX

  committed
  2eb6c20

  Copy full SHA for 2eb6c20

• Typo fixes and mention dependent hash maps in hash map documentation

  TwoFX

  committed
  1eb26e9

  Copy full SHA for 1eb26e9

• More map -> set replacements

  TwoFX

  committed
  2654f5e

  Copy full SHA for 2654f5e

• foldM docstring

  TwoFX

  committed
  3cd6ddf

  Copy full SHA for 3cd6ddf

• file -> module

  TwoFX

  committed
  a318eb1

  Copy full SHA for a318eb1

• Add valuesArray

  TwoFX

  committed
  edfa781

  Copy full SHA for edfa781

• Rework ofList and improve docstring for unit variants

  TwoFX

  committed
  e668766

  Copy full SHA for e668766

• Clarify behavior of HashSet.insert

  TwoFX

  committed
  424bfc7

  Copy full SHA for 424bfc7

• Add 'nothing to see here' docstrings to internal declarations

  TwoFX

  committed
  197cc2b

  Copy full SHA for 197cc2b

• Fix tests

  TwoFX

  committed
  b8dffae

  Copy full SHA for b8dffae

• Mention that hash maps use == and hash

  TwoFX

  committed
  6faa133

  Copy full SHA for 6faa133