Code

feat: recommended_spelling command#6869

Code

Merged

TwoFX merged 6 commits intomasterleanprover/lean4:masterfrom markus/notation-name-infraleanprover/lean4:markus/notation-name-infraCopy head branch name to clipboardFeb 3, 2025

+230-3

Commits

Commits on Jan 30, 2025

• feat: recommended_spelling command

  TwoFX

  committed
  e0ce2e6

  Copy full SHA for e0ce2e6

• fix test

  TwoFX

  committed
  9499b13

  Copy full SHA for 9499b13

Commits on Jan 31, 2025

• Apply suggestions from code review

  TwoFX

  committed
  b03a382

  Copy full SHA for b03a382

• Fix tests and documentation

  TwoFX

  committed
  4e26674

  Copy full SHA for 4e26674

Commits on Feb 1, 2025

• Improve command documentation as discussed in code review

  TwoFX

  committed
  e10ab60

  Copy full SHA for e10ab60

• I should get a VS Code extension that warns you if you commit a file that has unsaved changes

  TwoFX

  committed
  3326ff7

  Copy full SHA for 3326ff7