Idris ver 1.3.2 and Atom have been successfully installed on the Kubuntu version of Ubuntu Linux. The correct path to the idris binary has been put in the package settings in Atom. REPL works OK within Atom. The location of the idris binary is /home/tom/Documents . My 1 line source file called WordLength.idr file which is saved in Atom is given by:
allLengths : List String -> List Nat
(which is as described on page 56 of Brady’s book). The location where this file is saved is /home/tom/.cabal/bin/idris .
When I start up idris in the Linux command window the type check works as required and the ‘holes Main.allLengths’ is correctly reported.
However at the ‘Define’ stage as described on page 57, my problem is when I highlight allLengths with the cursor in the Atom editor and press Ctrl-Alt-A as required on page 57 there is no response from Atom when it should add the extra line as a skeleton definition to the source file in the editor.
I have tried adding various additional paths to the $PATH file in the vain hope that this would cure the problem.