search

wellecks / llmstep

llmstep: [L]LM proofstep suggestions in Lean 4.
MIT License
118 stars 15 forks source link

refactor addSuggestions #4

Closed kim-em closed 1 year ago

kim-em commented 1 year ago

These should make it easier to upstream.

(Apologies about the whitespace changes, I can revert those if desired. Most Lean projects have a .vscode/settings.json containing

{
  "editor.insertSpaces": true,
  "editor.tabSize": 2,
  "editor.rulers" : [100],
  "files.encoding": "utf8",
  "files.eol": "\n",
  "files.insertFinalNewline": true,
  "files.trimFinalNewlines": true,
  "files.trimTrailingWhitespace": true,
}
wellecks commented 1 year ago

The three PRs look great, thank you! I will merge them in soon