2

In agda-mode there is C-c C-d command to infer a type of expression. This is especially needed when we arrive at a type error! But exactly then this command doesn't work. I would guess that this is because the feature wants to evaluate the expression type in the context of the working file. Rightfully so - but is there a way to bypass it and for example find the expression type in the context of the longest typechecking prefix of a file?

I'm using agda-mode for vs-code but emacs tips are appreciated as well as they hopefully translate.

Also did I miss some feature to infer the type of expression at cursor? The way I use C-c C-d (infer type) is after this command I input the expression of interest manually (or paste it). Would be nice to get a type of the word the cursor points to.

zaabson
  • 151
  • 12
  • 3
    Maybe it would be worth knowing a bit more about your situation. For example, is there something stopping you commenting out the end of the file, or commenting out the ill typed expression and replacing it by a hole? – mudri Jan 06 '22 at 22:49
  • No, this is a valid solution just an inconvenient one. – zaabson Jan 06 '22 at 23:56
  • The fact that holes exist should result in files that always typecheck, I don't see why your situation would happen in a relevant development. Agda files are built step by step, and should typecheck throughout the whole process, until no more holes are left unfilled. – MrO Jan 07 '22 at 18:29

0 Answers0