이 문서는 토막글입니다.토막글 규정을 유의하시기 바랍니다.1. 개요2. 외부 링크1. 개요Agda는 Martin-Löf의 의존타입이론(dependent type theory)에 기반한 함수형 언어이자 증명보조기이다.프로그래밍 언어 Haskell의 영향을 받아 문법이 Haskell과 비슷하며 구현 또한 Haskell로 되어있다.2. 외부 링크The Agda Wiki 분류 증명보조기 함수형 언어