Agda の install の方法

Homebrew を使うのが良いそうです。

   brew install agda

GHCが入ってないなら、

   brew install ghc

install 先がどこかは、

    /opt/homebrew/Cellar/agda/

などになるので、

brew install の指示通りに ~/.agda に以下のファイルを置きます

    defaults   libraries

defaults の中には

    /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/standard-library.agda-lib

libraries の中には

    /opt/homebrew/Cellar/agda/2.6.2.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

 \Gl を入力してみる

入力できなかったら、

   キーボードショートカットの agda input を変更します

Emacs を先に入れます。

  brew tap caskroom/cask
  brew cask install emacs

~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。中のpathは正しいものに置き換えます。

  ssh amane "mkdir ~/.emacs.d"
  rsync -av ~/Downloads/init.el amane:~/.emacs.d/
  rsync -av ~/Downloads/eaw.el amane:~/.emacs.d/

GUI 側で使わないと文字化けすることがあるようです。Terminal で使いたい時には、

locale eaw が必要です。

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 というのもあるらしい。

neovim で、

nvim-agda が使えます。

ssh amane / ssh braun などで、

   singularity shell --shell=/bin/zsh /mnt/ie-virsh/singularity/agda/agda.sif

で動かすことができます

Agda のライブラリの説明をみていくと良い

 /opt/homebrew/Cellar/agda/2.6.2.2/lib/agda/README/Data/Nat.agda