-title: Agda の install の方法
Homebrew を使うのが良いそうです。
brew install agda
GHCが入ってないなら、
brew install ghc
install 先がどこかは、
/usr/local/Cellar/agda/2.6.1/lib/agda
などになるので、
brew install の指示通りに ~/.agda に以下のファイルを置きます
defaults libraries
defaults の中には
standard-library
libraries の中には
/usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
--VS-code
plugin から agda-mode を探して install
test.agda を作って
module test where
open import Data.Nat
a : ?
a = 1
として C-C C-L が通れば Ok
--Emacs
Emacs を先に入れます。
brew tap caskroom/cask
brew cask install emacs
~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
中のpathは正しいものに置き換えます。
init.el
GUI 側で使わないと文字化けすることがあるようです。Terminal で使いたい時には、
locale eaw
が必要です。
Emacs から使うので、Emacs も勉強しよう。
Emacs の使い方
C-C control と C を同時に押す
M-X esc を押してから X を押す
C-X C-F で、Agda1.agda file を開けます。
M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。
Space Emacs というのもあるらしい。
--vim
agda-vim
が使えます。