Adrian Lehmann comments

Results 20 comments of


                                            Adrian Lehmann

Modules missing in MacOSX release

Windowed unitary application

@cgranade Thank you for the suggestions, those indeed look more idiomatic - I'll update the PR

Table lookup

I'd vote for the name `ApplyTableLookup` as it will make the function more discoverable and its effects clearer. I'll update the PR

Use ViCaR to visualize terms in monoidal categories

We are definitely looking to expand the version compatibility. Right now the main "blocker" was our examples. If you plan on actively using our library, however, we could certainly look...

[protocol] Add `Search` support.

In 0.1.8 for Coq v8.18, I no longer see any results in messages when I use Search/Check/Print. This was not an issue previously on Coq 8.16 with lsp.

[protocol] Add `Search` support.

I only see it upon mouse-over, however there is no text cursor state (either before or after the period) where is see it.

[protocol] Add `Search` support.

https://github.com/ejgallego/coq-lsp/assets/26521502/0337e755-6bac-46fb-9e06-6f178b33fd15

[protocol] Add `Search` support.

This happens anywhere in the file

[protocol] Add `Search` support.

Adding https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/LSP.20search.20issue/near/419497086 as a reference

Feature request: High level Print-function

I think this would be a great idea to do! As for the specific implementation, the idea sounds great to be but I'm not sure if having the tuple have...