One of Idris’ coolest features is that of Interactive Editing, whereby the programmer develops their code in conjunction with the compiler. Afterall, the compiler knows more about your code than you will during development.

One of the important mantra’s described in the Idris Book is that of:

  1. Describe your program’s Types (datatypes type constructors and function type signatures);
  2. Define your program’s datatype constructors and function bodies;
  3. Refine goto 1 and fix any issues you have with your original definitions;

As you will see through-out the lectures, interactive editing helps us with the mantra of Type, Define, Refine and typed holes help use fill-in the blanks.

So while you can use Idris2 without an editor plugin, the experience is not good.

I strongly recommend that you get interactive editing working when studying the material from the lectures.