[ ソース: agda ]
パッケージ: elpa-agda2-mode (2.6.4.3-1)
elpa-agda2-mode に関するリンク
Debian の資源:
agda ソースパッケージをダウンロード:
メンテナ:
外部の資源:
- ホームページ [wiki.portal.chalmers.se]
類似のパッケージ:
依存型付けされた関数プログラミング言語 — emacs モード
Agda は依存型付けされた関数プログラミング言語です (Haskell の GADTs のよう な、帰納的定義型の種別を持ちますが、その型は型だけではなく値にインデックス されうる型です)。パラメータ付きモジュール、mixfix 演算子、Unicode 文字およ び Emacs 用対話的インターフェースを含みます (型検査器が、あなたのコードの 開発を補助します)。
Agda は定理証明支援系でもあります (証明を待ち、検査する対話的システムです)。 Agda は直観主義的な型理論に基づいています (スイスの論理学者 Per Martin-Löf によって開拓された構成的な数学の基礎理論です)。Coq, Epigram および NuPRL といった、依存型に基づいている他の定理証明支援系とも多くの類似点があります。
本パッケージには emacs の対話的 Agda 開発モードが含まれます。このモードは Agda コードを書くのに適しており、反復型開発、リファインメント、ケース解析な どの機能を提供します。
その他の elpa-agda2-mode 関連パッケージ
|
|
|
|
-
- dep: agda-bin (<< 2.6.4.3-1.1~)
- Agda へのコマンドラインインターフェース
- dep: agda-bin (>= 2.6.4.3-1)
-
- dep: dh-elpa-helper
- helper package for emacs lisp extensions
-
- dep: emacsen-common
- 全 Emacsen 用の共通機能
-
- dep: libghc-agda-dev (<< 2.6.4.3-1.1~)
- 依存型付けされた関数プログラミング言語
- dep: libghc-agda-dev (>= 2.6.4.3-1)
-
- rec: emacs (>= 46.0)
- GNU Emacs エディタ (メタパッケージ)
以下のパッケージによって提供される仮想パッケージでもあります: emacs-gtk, emacs-lucid, emacs-nox, emacs-pgtk
-
- enh: emacs
- GNU Emacs エディタ (メタパッケージ)
以下のパッケージによって提供される仮想パッケージでもあります: emacs-gtk, emacs-lucid, emacs-nox, emacs-pgtk
-
- enh: emacs24
- パッケージは利用できません