Code

feat: add simple Ordering lemmas#6821

Code

Merged

TwoFX merged 8 commits intomasterleanprover/lean4:masterfrom paul/ord-lemmasleanprover/lean4:paul/ord-lemmasCopy head branch name to clipboardJan 31, 2025

Commits

Commits on Jan 28, 2025

• add Ord and BEq lemmas

  datokrat

  committed
  53218f1

  Copy full SHA for 53218f1

• remove beq_eq_eq

  datokrat

  committed
  763ce15

  Copy full SHA for 763ce15

• more

  datokrat

  committed
  03ce020

  Copy full SHA for 03ce020

• derive LawfulBEq

  datokrat

  committed
  fdfe8f8

  Copy full SHA for fdfe8f8

Commits on Jan 29, 2025

• upstream lemmas from batteries

  datokrat

  committed
  44c3430

  Copy full SHA for 44c3430

• remove duplicated lemmas

  datokrat

  committed
  7749203

  Copy full SHA for 7749203

• apply suggestions

  datokrat

  committed
  7256be7

  Copy full SHA for 7256be7

Commits on Jan 30, 2025

• remove ?

  datokrat

  committed
  04e067b

  Copy full SHA for 04e067b