Code

feat: attribute [simp ←]#5870

Code

Merged

nomeata merged 12 commits intomasterleanprover/lean4:masterfrom joachim/simp-attrib-modifiersleanprover/lean4:joachim/simp-attrib-modifiersCopy head branch name to clipboardOct 29, 2024

+130-12

Commits

Commits on Oct 28, 2024

• Refactor syntax

  nomeata

  committed
  1d74f81

  Copy full SHA for 1d74f81

• Revert "Refactor syntax", due to boostrapping headaches

  Show description for 541c1b1
  nomeata

  committed
  541c1b1

  Copy full SHA for 541c1b1

• Prepare stage0

  nomeata

  committed
  cb0bb71

  Copy full SHA for cb0bb71

• chore: update stage0

  nomeata

  committed
  a9a03b0

  Copy full SHA for a9a03b0

• Change attr syntax

  nomeata

  committed
  bed78c6

  Copy full SHA for bed78c6

• Actually set inv flag

  nomeata

  committed
  e81d8b9

  Copy full SHA for e81d8b9

• Test case, make it work

  nomeata

  committed
  215185c

  Copy full SHA for 215185c

• Also fix registerSimpAttr

  nomeata

  committed
  29830d5

  Copy full SHA for 29830d5

• Revert "chore: update stage0"

  Show description for 790ff93
  nomeata

  committed
  790ff93

  Copy full SHA for 790ff93

• Try prefer_native

  nomeata

  committed
  03b6034

  Copy full SHA for 03b6034

Commits on Oct 29, 2024

• Fix docs

  nomeata

  committed
  5d4a657

  Copy full SHA for 5d4a657

• Should save before pushing

  nomeata

  committed
  2145fb4

  Copy full SHA for 2145fb4