How to check type of term under cursor

[langfield]

How do you check the type of the highlighted term using cornelis?

[isovector]

I don't think you can. Does this functionality exist in emacs?

[langfield]

Oh, too bad! Not sure about emacs. Is this a limitation imposed by the compiler?

[isovector]

Cornelis is just an interface between vim and the compiler. I'm happy to implement any functionality that is missing in parity with emacs, but i can't work miracles (unfortunately!)

A good temporary workaround here is to replace the term you care about with a question mark and reload.

On November 18, 2023 1:23:18 p.m. PST, langfield @.***> wrote:

Oh, too bad! Not sure about emacs. Is this a limitation imposed by the compiler?

-- Reply to this email directly or view it on GitHub: https://github.com/isovector/cornelis/issues/127#issuecomment-1817646189 You are receiving this because you commented.

Message ID: @.***>

[langfield]

I see, I see. Tell me, is it possible to get it to auto-load on each edit, similar to how HLS works?

[googleson78]

How do you check the type of the highlighted term using cornelis? I don't think you can. Does this functionality exist in emacs?

I think it doesn't exist directly, but there is "Infer (deduce) type, which should be relatively easy to wire up to work with the item under the cursor. Not sure it's a good idea in general though - putting stuff in a hole and then looking at types results in a better UX from my experience using agda in emacs.

I see, I see. Tell me, is it possible to get it to auto-load on each edit, similar to how HLS works?

This should be trivially doable with an autocmd, e.g. something like

autocmd TextChangedI ?* <call cornelis reload>

[langfield]

Seems like this has been answered satisfactorily! Thanks @googleson78 @isovector! 💯