すべてのオプション
buster  ] [  bullseye  ] [  bookworm  ] [  trixie  ] [  sid  ]
[ ソース: agda  ]

パッケージ: elpa-agda2-mode (2.6.2.2-1.1)

elpa-agda2-mode に関するリンク

Screenshot

Debian の資源:

agda ソースパッケージをダウンロード:

メンテナ:

外部の資源:

類似のパッケージ:

依存型付けされた関数プログラミング言語 — emacs モード

Agda は依存型付けされた関数プログラミング言語です (Haskell の GADTs のよう な、帰納的定義型の種別を持ちますが、その型は型だけではなく値にインデックス されうる型です)。パラメータ付きモジュール、mixfix 演算子、Unicode 文字およ び Emacs 用対話的インターフェースを含みます (型検査器が、あなたのコードの 開発を補助します)。

Agda は定理証明支援系でもあります (証明を待ち、検査する対話的システムです)。 Agda は直観主義的な型理論に基づいています (スイスの論理学者 Per Martin-Löf によって開拓された構成的な数学の基礎理論です)。Coq, Epigram および NuPRL といった、依存型に基づいている他の定理証明支援系とも多くの類似点があります。

本パッケージには emacs の対話的 Agda 開発モードが含まれます。このモードは Agda コードを書くのに適しており、反復型開発、リファインメント、ケース解析な どの機能を提供します。

その他の elpa-agda2-mode 関連パッケージ

  • 依存
  • 推奨
  • 提案
  • enhances

elpa-agda2-mode のダウンロード

すべての利用可能アーキテクチャ向けのダウンロード
アーキテクチャ パッケージサイズ インストールサイズ ファイル
all 49.8 kB208.0 kB [ファイル一覧]