Code

feat: improve grind failure message#6633

Code

Merged

leodemoura merged 6 commits intomasterleanprover/lean4:masterfrom grind_ppleanprover/lean4:grind_ppCopy head branch name to clipboardJan 14, 2025

+283-84

Commits

Commits on Jan 13, 2025

• chore: workaround for simulating hovering information

  leodemoura

  committed
  5c99d80

  Copy full SHA for 5c99d80

• refactor: return List Goal at Grind.main

  leodemoura

  committed
  27dcf54

  Copy full SHA for 27dcf54

Commits on Jan 14, 2025

• chore: mark it as implicit to improve pretty printing

  leodemoura

  committed
  e08f10e

  Copy full SHA for e08f10e

• feat: improve grind failure message

  leodemoura

  committed
  51055e7

  Copy full SHA for 51055e7

• chore: fix tests

  leodemoura

  committed
  fb11fef

  Copy full SHA for fb11fef

• chore: fix message

  leodemoura

  committed
  a0de63e

  Copy full SHA for a0de63e