Currently, we have vendored completions/lean-abbreviations.json, which is sourced from the Lean extension.
In order to avoid vendoring and decrease friction, we should:
- Introduce a dependency to
lean4-unicode-input
- Include a build step that produces the merged file with our symbols + Lean's
- Remove the unneeded files from git
Currently, we have vendored completions/lean-abbreviations.json, which is sourced from the Lean extension.
In order to avoid vendoring and decrease friction, we should:
lean4-unicode-input