Code

chore: upstream Nat.binaryRec#3756

Code

Open

FR-vdash-bot wants to merge 7 commits intoleanprover:masterleanprover/lean4:masterfrom FR-vdash-bot:binaryRecFR-vdash-bot/lean4:binaryRecCopy head branch name to clipboard

+213-108

Commits

Commits on Apr 25, 2024

• chore: upstream Nat.binaryRec

  FR-vdash-bot

  committed
  f66834f

  Copy full SHA for f66834f

• upstream bitCasesOn_bit

  FR-vdash-bot

  committed
  93d85bb

  Copy full SHA for 93d85bb

• missing @[simp]

  FR-vdash-bot

  authored
  ac17fc1

  Copy full SHA for ac17fc1

• docs, do not use the name Nat.bit_decomp

  FR-vdash-bot

  committed
  aaeb7aa

  Copy full SHA for aaeb7aa

• remove eqRec_eq_cast Nat.binaryRec_of_ne_zero

  FR-vdash-bot

  committed
  26c483f

  Copy full SHA for 26c483f

Commits on May 8, 2024

• move Bool.toNat back

  FR-vdash-bot

  committed
  0004d42

  Copy full SHA for 0004d42

• fix

  FR-vdash-bot

  committed
  3eb032a

  Copy full SHA for 3eb032a