Idris
Idris
Idris는 Agda와 함께 대표적인 의존 타입(dependent type) 언어예요. 타입이 값에 의존할 수 있어 정밀한 명세를 프로그램에 직접 녹여낼 수 있고, 타입 검사를 통과한 프로그램은 그 명세를 만족함을 보장해요. 공식 문서 reference 와 tutorial 은 구문·타입·인터페이스·정리 증명·REPL 등 Idris 개발에 필요한 전반을 다룹니다.
Idris는 Agda와 함께 대표적인 의존 타입(dependent type) 언어예요. 타입이 값에 의존할 수 있어 정밀한 명세를 프로그램에 직접 녹여낼 수 있고, 타입 검사를 통과한 프로그램은 그 명세를 만족함을 보장해요. 공식 문서 reference 와 tutorial 은 구문·타입·인터페이스·정리 증명·REPL 등 Idris 개발에 필요한 전반을 다룹니다.