Code

feat: binderNameHint#6947

Code

Merged

nomeata merged 13 commits intomasterleanprover/lean4:masterfrom joachim/binderNameHintleanprover/lean4:joachim/binderNameHintCopy head branch name to clipboardFeb 6, 2025

+305

Commits

Commits on Feb 4, 2025

• feat: binderNameHint

  nomeata

  committed
  222dd6e

  Copy full SHA for 222dd6e

• Also test dsimp (but already works)

  nomeata

  committed
  82e15ff

  Copy full SHA for 82e15ff

• Actually save file

  nomeata

  committed
  4dd212d

  Copy full SHA for 4dd212d

• Update tests (improved simp trace formatting)

  nomeata

  committed
  f10246d

  Copy full SHA for f10246d

• More test updates

  nomeata

  committed
  fb8a256

  Copy full SHA for fb8a256

• set_option Elab.async false -- for stable message ordering in #guard_msgs

  nomeata

  committed
  97f6ff0

  Copy full SHA for 97f6ff0

• undo simp tracing changes

  nomeata

  committed
  81a27d9

  Copy full SHA for 81a27d9

• PR splitting mistake

  nomeata

  committed
  7c98ec1

  Copy full SHA for 7c98ec1

Commits on Feb 5, 2025

• More docs and tests

  nomeata

  committed
  4bf9b8f

  Copy full SHA for 4bf9b8f

• Merge branch 'nightly' of https://github.com/leanprover/lean4 into joachim/binderNameHint

  nomeata

  committed
  548b268

  Copy full SHA for 548b268

Commits on Feb 6, 2025

• Ensure that simp and dsimp pre-rewrite with binderNameHint

  Show description for 86463de
  nomeata

  committed
  86463de

  Copy full SHA for 86463de

• Freshen name when binder is not a binder

  nomeata

  committed
  0dfb8e1

  Copy full SHA for 0dfb8e1

• Test adding macro scopes

  nomeata

  committed
  2bbffb9

  Copy full SHA for 2bbffb9