Code

feat: add list function and lemmas#987

Code

Open

chabulhwi wants to merge 21 commits intoleanprover-community:mainleanprover-community/batteries:mainfrom chabulhwi:add-more-list-lemmaschabulhwi/batteries:add-more-list-lemmasCopy head branch name to clipboard

Commits

Commits on Oct 15, 2024

• feat: add lemmas about lists

  Show description for 344bd60
  chabulhwi

  committed
  344bd60

  Copy full SHA for 344bd60

• feat: add more lemmas about lists

  Show description for 87f4b94
  chabulhwi

  committed
  87f4b94

  Copy full SHA for 87f4b94

• style: avoid using @ symbol

  Show description for 02599d9
  

  chabulhwi

  and

  fgdorais

  committed
  02599d9

  Copy full SHA for 02599d9

• refactor: remove implicit instances of theorem

  chabulhwi

  committed
  f39e00a

  Copy full SHA for f39e00a

• refactor: put theorem in section

  chabulhwi

  committed
  2d30498

  Copy full SHA for 2d30498

• feat: add List.commonPrefix and its lemmas

  Show description for 6b39d44
  chabulhwi

  committed
  6b39d44

  Copy full SHA for 6b39d44

• refactor: rename and restate theorem

  Show description for ce38099
  chabulhwi

  committed
  ce38099

  Copy full SHA for ce38099

• chore: move definition to another file

  Show description for 6b7c0e4
  chabulhwi

  committed
  6b7c0e4

  Copy full SHA for 6b7c0e4

Commits on Oct 16, 2024

• feat: add theorem List.commonPrefix_comm

  Show description for ab8e65a
  

  chabulhwi

  and

  kmill

  committed
  ab8e65a

  Copy full SHA for ab8e65a

• style: avoid using Decidable.em directly

  Show description for 9e0d971
  

  chabulhwi

  and

  kmill

  committed
  9e0d971

  Copy full SHA for 9e0d971

• refactor: golf proofs

  Show description for d257184
  

  chabulhwi

  and

  kmill

  committed
  d257184

  Copy full SHA for d257184

• Revert "refactor: golf proofs"

  Show description for fa83dc7
  chabulhwi

  committed
  fa83dc7

  Copy full SHA for fa83dc7

• Revert "style: avoid using Decidable.em directly"

  Show description for ffbd01f
  chabulhwi

  committed
  ffbd01f

  Copy full SHA for ffbd01f

• Revert "feat: add theorem List.commonPrefix_comm"

  Show description for 49f306e
  chabulhwi

  committed
  49f306e

  Copy full SHA for 49f306e

• Revert "chore: move definition to another file"

  Show description for 0e6bfd8
  chabulhwi

  committed
  0e6bfd8

  Copy full SHA for 0e6bfd8

• Revert "refactor: rename and restate theorem"

  Show description for 10a0c0d
  chabulhwi

  committed
  10a0c0d

  Copy full SHA for 10a0c0d

• Revert "feat: add List.commonPrefix and its lemmas"

  Show description for 75ec590
  chabulhwi

  committed
  75ec590

  Copy full SHA for 75ec590

• Revert "refactor: put theorem in section"

  Show description for f3a2b95
  chabulhwi

  committed
  f3a2b95

  Copy full SHA for f3a2b95

• Revert "refactor: remove implicit instances of theorem"

  Show description for 1d57ce4
  chabulhwi

  committed
  1d57ce4

  Copy full SHA for 1d57ce4

• chore: remove theorem

  Show description for 7c5ef34
  chabulhwi

  committed
  7c5ef34

  Copy full SHA for 7c5ef34

Commits on Oct 19, 2024

• Merge branch 'main' into add-more-list-lemmas

  fgdorais

  authored
  fa178b5

  Copy full SHA for fa178b5