2019-01-28から1日間の記事一覧

Agda のモジュール読み込みのエラー

Agda のモジュール読み込みのエラー Agda 2.5.2 で import my-module-file as M のようにしてファイルを開こうとすると、 Module cannot be imported since it has open interaction points when scope checking the declaration import my-module-file as M…

bash の補完機能は inputrc で

bash の補完機能で大文字と小文字の区別をなくす bash でファイル名をタブで補完するとき、Windows の Git Bash みたいに大文字小文字 の補完を自動でやってくれるようにしました。 set completion-ignore-case on というのを ~/.inputrc というところに書い…