Similarly to the Coq and Lean programming languages, Agda, which also doubles up as a proof assistant, is better used with more support than just a plain LS (#86) and a tree-sitter grammar (already in visimp).
Yeah I think an extra field for binds on the specific layer is what we've always done.
Using the sample bindings (or something else, as long as it makes sense) is a good idea.
Similarly to the Coq and Lean programming languages, Agda, which also doubles up as a proof assistant, is better used with more support than just a plain LS (#86) and a tree-sitter grammar (already in visimp).
https://github.com/isovector/cornelis is both actually developed and featureful.
@lucat1 should we add a config field to the
agda
layer for bindings? Should we add the sample bindings in the README as default bindings?