Sébastien Michelland

Add instant and prefix-based completion (#36)

1

This PR implements a rough version of the features proposed in the linked issue. - The prefix feature is supported by adding a `symbol_by_unique_prefix()` function in `mathsymbols.py`. The function only...

Option to insert instantly when not ambiguous?

1

First of all, I really love this package, thank your for keeping it up. :D A very efficient behavior I've found on other editors is to insert escapes more eagerly...

https://github.com/opencompl/lean-mlir/commit/cf7d6828ef52a54339a2dc7aa6345bfd4d56c274 updates to a nightly after the implementation of typed syntax. It enriches the types in some places but mostly adds bypasses, and some of these reveal parsing errors I...

The EDSL is now more powerful, and keeping both systems with different parsing power seems like it could be a problem in the longer run (and I don't think you...