프로그래밍 언어로서의 Agda [닫기]

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

  •  13-12-2019
  •  | 
  •  

문제

나는 Agda를 증명 시스템으로 사용하는 것에 대한 유용한 정보를 많이 찾았습니다.나는 Agda를 사용하여 유용한 프로그램을 작성하는 방법에 대한 정보를 거의 찾지 못했습니다.최신 버전의 Agda로 컴파일되는 "hello world" 예제도 찾을 수 없습니다.

그래서,

  1. 프로그래밍 언어로서 Agda에 대한 좋은 튜토리얼이 있나요?

  2. 프로그래밍 언어로 사용하기 위한 보다 성숙한 문서가 있는 비슷한 성격의 다른 언어(게으른 함수 종속 유형)가 있습니까?(Coq에서 수많은 훌륭한 문서를 찾았지만 "Hello World"는 없습니다).

도움이 되었습니까?

해결책

Agda에서 문자열을 인쇄하려면 다음이 필요합니다. 표준 라이브러리."hello world" 예제를 찾을 수 있습니다. 여기 Agda 2.2.6 및 std lib 0.3용.이 예제는 현재 Agda 2.3.0 및 std lib 0.6에서는 작동하지 않습니다.std lib 0.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. "./hello.agda"에 저장하세요.
  2. lib-0.6.tar.gz를 다운로드하고 DIR이라는 곳에 압축을 푼다.
  3. CD DIR/ffi && 카발 설치
  4. agda -i DIR/src -i .-c hello.agda

ghc-7.4.2 및 cabal-1.16.0이 설치된 MacOSX Lion에서는 이 예제가 제대로 작동합니다.크기가 19.1M인 "hello"라는 실행 프로그램을 얻었습니다.

다른 팁

이는 초기 단계이지만 하루는 유용한 리소스가 될 수 있습니다.

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

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 StackOverflow
scroll top