Code

feat: Add String.isPrefixOf theorems#809

Code

Open

tjf801 wants to merge 16 commits intoleanprover-community:mainleanprover-community/batteries:mainfrom tjf801:isPrefixOf-theorems-2tjf801/batteries:isPrefixOf-theorems-2Copy head branch name to clipboard

+206

Commits

Commits on May 6, 2024

• Add lemmas necessary for isPrefixOf proofs

  Show description for 0489657
  tjf801

  committed
  0489657

  Copy full SHA for 0489657

• Add isPrefixOf proofs

  tjf801

  committed
  b4afe21

  Copy full SHA for b4afe21

Commits on May 13, 2024

• add info about unusedHavesSuffices lint

  Show description for b0ac67f
  

  tjf801

  and

  kim-em

  authored
  b0ac67f

  Copy full SHA for b0ac67f

• remove unnecessary data_append theorem

  tjf801

  committed
  9c1bf76

  Copy full SHA for 9c1bf76

• Merge branch 'main' into isPrefixOf-theorems

  tjf801

  committed
  10a27cc

  Copy full SHA for 10a27cc

• Revert "remove unnecessary data_append theorem"

  Show description for cc2174d
  tjf801

  committed
  cc2174d

  Copy full SHA for cc2174d

• make cons_append not @[simp]

  tjf801

  committed
  c7d6250

  Copy full SHA for c7d6250

Commits on May 18, 2024

• Merge branch 'leanprover-community:main' into isPrefixOf-theorems

  tjf801

  authored
  8895e19

  Copy full SHA for 8895e19

Commits on May 21, 2024

• Add substrEq_cons

  tjf801

  committed
  c2eedba

  Copy full SHA for c2eedba

• Add isPrefixOf lemmas

  Show description for 2aabdc1
  tjf801

  committed
  2aabdc1

  Copy full SHA for 2aabdc1

Commits on May 23, 2024

• Keep TODOs in for future unproven string theorems

  Show description for 8b65f75
  

  tjf801

  and

  chabulhwi

  committed
  8b65f75

  Copy full SHA for 8b65f75

• Fix linter fail

  Show description for c0e34b1
  tjf801

  committed
  c0e34b1

  Copy full SHA for c0e34b1

• fix unusedHavesSuffices x3

  tjf801

  committed
  4c1b33e

  Copy full SHA for 4c1b33e

Commits on Jun 10, 2024

• Merge branch 'main' into isPrefixOf-theorems-2

  tjf801

  committed
  9a6f10d

  Copy full SHA for 9a6f10d

Commits on Jun 14, 2024

• Update isPrefixOf lemmas for v4.9.0

  Show description for e5bb255
  tjf801

  committed
  e5bb255

  Copy full SHA for e5bb255

Commits on Oct 1, 2024

• chore: merge main and trigger Mathlib check

  fgdorais

  committed
  3142684

  Copy full SHA for 3142684