Conversation

Special syntax for asking the compiler what it thinks the type of an expression should be, and what locals exist to write it, without running/compiling the code. I've heard that Idris has this and that it's amazing. Only works with very strictly typed languages though.
1
7
Yeah, typed holes are great, especially when you can run code with holes still present. See Agda, and Haskell as some other examples. I think Agda is one of the best as the programmer can insert extra info into the hole to guide the editing interaction.
2
6
I also like how in Coq and Lean you can use commands in the source file to query the type of something, etc. As noted here, combined with intellisense it feels a bit like a more tightly integrated REPL:
Quote Tweet
Replying to @defnotbeka
Typed holes like in Agda, Where you get syntax that you can use to manipulate half-finished code (inferring programs and case splitting etc). Commands to #check and #eval stuff in Lean, which combined with intellisense lets you have a REPL-like experience within a source file.