The Atom editor has great support for Idris. When I tried to get into it, I happened upon a rather nasty longstanding bug that made it impossible for me to use it, I couldn’t type backslash on a Swedish keyboard. Atom defines loads of Ctrl-Alt keybindings that overloads the AltGr bindings commonly found on European keyboards.

To fix it I did the following:

• I toggled the keybinding resolver (in the packages menu) to see exactly what the keybinding is named and what it’s triggering.
• I found that the keybinding was ctrl-alt-= and that it resized a pane, hardly an essential thing so I didn’t need to allocate a new binding for it.
• I added the following to the user bindings file (choose ‘Open yor keymap’ in the files menu) to make it use the native keybinding for that combo:

    'atom-text-editor':
        'ctrl-alt-=': 'native!'

• Adventure Post-mortem

  How do you fit all this into 4096 bytes of ROM and 128 bytes of RAM?

  A good data structure, and efficient coding.

• Let’s write a PDF file

  Ange Albertini walks through creating a basic PDF file from scratch. He also makes great posters.

• Coding for Types: The Universe Pattern in Idris

  Great talk by David Christiansen about the Universe pattern (creating a Universe type that encodes a set of types as values that can then be pattern matched over).