WindowsのREPL Initファイル

Question

Windowsのidris REPLのinitスクリプトはどこに置くことができますか？私は

C:\Users\frankr85\Application Data\idris\repl\init 

でコマンドを入れた場合

は、コンテンツがロードされていません。

アイデア？

Answer 1

見つけました。それは - 少なくとも私にとっては - ここに：

C:\Users\frankr85\AppData\Roaming\idris\repl 

Answer 2

ディレクトリは%appdata%/idris/repl/で、initファイルはinitです。 つまり%appdata%/idris/repl/init