separate lean 4 `sorry` fill into single goal and multiple goal alternatives

Julian / lean.nvim

neovim support for the Lean theorem prover

MIT License

248 stars 25 forks source link

separate lean 4 `sorry` fill into single goal and multiple goal alternatives #307

Closed gihanmarasingha closed 11 months ago

gihanmarasingha commented 11 months ago

If there is a single remaining goal, the sorry fill code just adds a sorry in the next line. If there are multiple goals, a · sorry is added. Indentation is adjusted accordingly.

Tests are provided.

Julian commented 11 months ago

Looks great!