Agda를 증명 시스템으로 사용하는 것에 대한 많은 유용한 정보를 발견했습니다. Agda를 사용하여 쓸만한 프로그램을 작성하는 것에 관한 정보는 거의 발견되지 않았습니다. Agda의 최신 버전으로 컴파일되는 "hello world"예제를 찾을 수 없습니다. Agda 프로그래밍 언어
그래서,이 있습니까?
프로그래밍 언어로 사용하기에 더 성숙한 문서를 가지고있는 유사한 성격의 (게으른 기능이있는 유형이 다른) 다른 언어가 있습니까? (나는 Coq에 대한 수많은 훌륭한 문서를 찾았지만, 다시 "Hello World"는 없다.)
이 AGDA에서 문자열을 인쇄하려면, 당신은 std lib이 필요합니다. Agda 2.2.6 및 std lib 0.3에 대해 "안녕하세요 세상"예제 here을 찾을 수 있습니다. 이 예제는 현재 Agda 2.3.0 및 std lib 0.6에서는 작동하지 않습니다. 나는 0.6 lib에는 표준의 일부 소스를 읽고, 다음 중 하나가 작동하는 것을 발견 :
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!")
는 당신이 필요로 컴파일하기 위해
ghc-7.4.2 및 cabal-1.16.0을 사용하는 MacOSX Lion에서는이 예제가 올바르게 작동합니다. 나는 19.1M 크기의 "hello"라는 실행 프로그램을 얻는다.
Hello world @ 20M is pretty 말도 안되는 소리 –
도청 설치를 왜해야합니까? 또한 허가를 요청합니다. 또한 내가 줄 때 내 관리자 암호는 여전히 허가가 거부되었다고 말합니다. –
FFI 모듈을 설치하지 않고 사용할 수 있습니까? –
얼마나 열심히 보았습니까? 1 분 안에 [자습서] (http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)를 발견했습니다. 첫 번째 PDF는 마지막에 안녕하세요. (4.3 절). –
아아, 현재 Agda로 컴파일되지 않습니다. ( – Owen
당신을 [Idris] (http://idris-lang.org/)로 안내 할 수 있으며, 기능적으로 의존적으로 타이핑되어 명시적인 게으름 기호가 있습니다. 하스켈 (그리고 Agda)은 – Vitus