Code

Feature: Diagnostic Hints#29

Code

Merged

onriv merged 9 commits intomainonriv/lean4ij:mainfrom feat/eol-hintsonriv/lean4ij:feat/eol-hintsCopy head branch name to clipboardOct 19, 2024

+409-54

Commits

Commits on Oct 16, 2024

• Add actions for inserting and deleting ranges of goal hints

  enigmurl

  committed
  4e8cc64

  Copy full SHA for 4e8cc64

• Make goal hints work in both tactic and non tactic mode

  enigmurl

  committed
  c8bd242

  Copy full SHA for c8bd242

• minor comment changes

  enigmurl

  committed
  21a16ac

  Copy full SHA for 21a16ac

Commits on Oct 18, 2024

• Add basic diagnostic hints

  enigmurl

  committed
  6e6e273

  Copy full SHA for 6e6e273

• Add diagnostic hints to settings page

  enigmurl

  committed
  6b3f561

  Copy full SHA for 6b3f561

Commits on Oct 19, 2024

• Fix refreshing of diagnostic hints

  enigmurl

  committed
  bcdeaca

  Copy full SHA for bcdeaca

• Finish diagnostic hints

  enigmurl

  committed
  f9e5cb5

  Copy full SHA for f9e5cb5

• Fix typo in id of plugin.xml

  enigmurl

  committed
  aafc78a

  Copy full SHA for aafc78a

• Fix collapsing issue of inlay hints

  enigmurl

  committed
  772ed7e

  Copy full SHA for 772ed7e