[ ソース: agda ]
パッケージ: agda-bin (2.5.4.1-3 など)
agda-bin に関するリンク
Debian の資源:
agda ソースパッケージをダウンロード:
メンテナ:
外部の資源:
- ホームページ [wiki.portal.chalmers.se]
類似のパッケージ:
Agda へのコマンドラインインターフェース
Agda は依存型付けされた関数プログラミング言語です (Haskell の GADTs のよう な、帰納的定義型の種別を持ちますが、その型は型だけではなく値にインデックス されうる型です)。パラメータ付きモジュール、mixfix 演算子、Unicode 文字およ び Emacs 用対話的インターフェースを含みます (型検査器が、あなたのコードの 開発を補助します)。
Agda は定理証明支援系でもあります (証明を待ち、検査する対話的システムです)。 Agda は直観主義的な型理論に基づいています (スイスの論理学者 Per Martin-Löf によって開拓された構成的な数学の基礎理論です)。Coq, Epigram および NuPRL といった、依存型に基づいている他の定理証明支援系とも多くの類似点があります。
本パッケージは Agda プログラムの型チェックおよびコンパイル用のコマンドライ ンプログラムを提供します。Agda ソースコードからハイパーリンクおよびハイライ ト付きの HTML ファイルを生成する機能もあります。
その他の agda-bin 関連パッケージ
|
|
|
|
-
- dep: libatomic1 (>= 4.8)
- __atomic ビルトイン関数を提供するサポートライブラリ
-
- dep: libc6 (>= 2.27) [i386 以外]
- GNU C ライブラリ: 共有ライブラリ
以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb
- dep: libc6 (>= 2.28) [i386]
-
- dep: libffi6 (>= 3.0.4) [arm64 以外]
- Foreign Function Interface ランタイムライブラリ
- dep: libffi6 (>= 3.2) [arm64]
-
- dep: libgmp10
- 多倍長精度演算ライブラリ
-
- dep: libtinfo6 (>= 6)
- 端末を扱う低レベルの terminfo 共有ライブラリ
-
- dep: zlib1g (>= 1:1.1.4)
- 圧縮ライブラリ - ランタイム
-
- rec: libghc-agda-dev (<< 2.5.4.1+~)
- 依存型付けされた関数プログラミング言語
- rec: libghc-agda-dev (>= 2.5.4.1)
-
- sug: elpa-agda2-mode
- 依存型付けされた関数プログラミング言語 — emacs モード