プログラミング言語としてのAgda[終了しました]

StackOverflow https://stackoverflow.com//questions/9692445

  •  13-12-2019
  •  | 
  •  

質問

私は証拠システムとしてAgdaを使用する上で多くの有用な情報を発見しました。使用可能なプログラムを書くためにAgdaを使用することに関する情報は事実上見つかりませんでした。できないもの"hello world"の例を編集すると最新バージョンのAgda.

だから,

  1. プログラミング言語としてのAgdaに関する良いチュートリアルはありますか？

  2. プログラミング言語として使用するためのより成熟したドキュメントを持っている同様の性質の他の言語（遅延関数依存型）はありますか？(このトンの文書-コックは、ただしこの場合にも、"こんにちはます。

役に立ちましたか？

解決

Agdaで文字列を印刷するには、次のものが必要です std lib.き"hello world"の例 ここに Agda2.2.6およびstd lib0.3の場合。この例は、現在のAgda2.3.0とstd lib0.6では機能しません。私はstd lib0.6のいくつかのソースを読んで、次のものが動作することがわかります:

module hello where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring; String)
open import Foreign.Haskell using (Unit)

main : IO Unit
main = putStrLn (toCostring "Hello, Agda!")

それをコンパイルするには、次のものが必要です

  1. "に保存します。/こんにちは.アグダ"
  2. ダウンロードlib-0.6.タールgz、そしてどこかにそれを解凍し、DIRと言う
  3. cdディレクトリ/ffi&&cabalインストール
  4. agda-i DIR/src-i.-cこんにちは.アグダ

Ghc-7.4.2とcabal-1.16.0を搭載した私のMacOSX Lionでは、この例は正常に動作します。または、実行プログラム名"こんにちは"サイズ19.1M.

他のヒント

これは初期のものですが、1日が有用なリソースになる可能性があります:

https://github.com/liamoc/learn-you-an-agda

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top