12 lines
702 B
Plaintext
12 lines
702 B
Plaintext
Agda is a dependently typed functional programming language: It has
|
|
inductive families, which are similar to Haskell's GADTs, but they can be
|
|
indexed by values and not just types. It also has parameterised modules,
|
|
mixfix operators, Unicode characters, and an interactive Emacs interface
|
|
(the type checker can assist in the development of your code).
|
|
|
|
Agda is also a proof assistant: It is an interactive system for writing and
|
|
checking proofs. Agda is based on intuitionistic type theory, a foundational
|
|
system for constructive mathematics developed by the Swedish logician Per
|
|
Martin-Lof. It has many similarities with other proof assistants based on
|
|
dependent types, such as Coq, Epigram and NuPRL.
|