[ ソース: agda-stdlib ]
パッケージ: agda-stdlib-doc (2.1-3)
agda-stdlib-doc に関するリンク
Debian の資源:
agda-stdlib ソースパッケージをダウンロード:
メンテナ:
外部の資源:
- ホームページ [wiki.portal.chalmers.se]
類似のパッケージ:
Agda 用標準ライブラリ — ドキュメンテーション
Agda は依存型付けされた関数プログラミング言語です (Haskell の GADTs のよう な、帰納的定義型の種別を持ちますが、その型は型だけではなく値にインデックス されうる型です)。パラメータ付きモジュール、mixfix 演算子、Unicode 文字およ び Emacs 用対話的インターフェースを含みます (型検査器が、あなたのコードの 開発を補助します)。
Agda は定理証明支援系でもあります (証明を待ち、検査する対話的システムです)。 Agda は直観主義的な型理論に基づいています (スイスの論理学者 Per Martin-Löf によって開拓された構成的な数学の基礎理論です)。Coq, Epigram および NuPRL といった、依存型に基づいている他の定理証明支援系とも多くの類似点があります。
Agda 標準ライブラリには数多くの標準的データ構造と証明パターンが含まれます。 提供されるモジュールには以下のようなものがあります。
- Algebra: 抽象的代数構造についての指定と推論 - Category: 関数型プログラムで圏論のイディオムを使用 - Coinduction: 余帰納的プログラミングのサポート - Data: データ型についてのデータ型とプロパティ - Foreign: 外部関数インターフェースへの関連付け - Induction: 汎用帰納フレームワーク - IO: 入出力関連関数 - Level: Universe levels - Relations: 関係についてのプロパティと証明 - Size: サイズ付き型機構で使われるサイズ
本パッケージには、ハイパーリンク付きライブラリドキュメンテーションが含まれ ます。