fb16dfecae
Commit b7f05445c0 has added WWW entries to port Makefiles based on
WWW: lines in pkg-descr files.
This commit removes the WWW: lines of moved-over URLs from these
pkg-descr files.
Approved by: portmgr (tcberner)
11 lines
702 B
Text
11 lines
702 B
Text
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.
|