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.
