Content deleted Content added
No edit summary Tags: Visual edit Mobile edit Mobile web edit |
m Disambiguating links to Coq (link changed to Coq (software); link changed to Coq (software); link changed to Coq (software); link changed to Coq (software)) using DisamAssist. |
||
Line 18:
| influenced = [[Idris (programming language)|Idris]]
| programming language = [[Haskell (programming language)|Haskell]]
| influenced by = [[Coq (software)|Coq]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]]
| license = [[BSD licenses|BSD-like]]<ref>[http://code.haskell.org/Agda/LICENSE Agda license file]</ref>
| file ext = <code>.agda</code>, <code>.lagda</code>, <code>.lagda.md</code>, <code>.lagda.rst</code>, <code>.lagda.tex</code>
Line 27:
</ref> The original Agda system was developed at Chalmers by Catarina Coquand in 1999.<ref>{{Cite web |url = http://ocvs.cfv.jp/Agda/index.html |title = Agda: An Interactive Proof Editor |access-date = 2014-10-20 |archive-url = https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/index.html |archive-date = 2011-10-08 |url-status = dead }}</ref> The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.
Agda is also a [[proof assistant]] based on the [[propositions-as-types]] paradigm, but unlike [[Coq (software)|Coq]], has no separate [[Tactic (computer science)|tactics]] language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as [[data type]]s, [[pattern matching]], [[Record (computer science)|records]], [[let expression]]s and modules, and a [[Haskell (programming language)|Haskell]]-like syntax. The system has [[Emacs]], [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |first1 = Catarina |last1 = Coquand |first2 = Dan |last2 = Synek |first3 = Makoto |last3 = Takeyama |title = An Emacs interface for type directed support constructing proofs and programs |conference = European Joint Conferences on Theory and Practice of Software 2005 |url = https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |archive-url = https://web.archive.org/web/20110722063632/https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |url-status = dead |archive-date = 2011-07-22 }}</ref><ref>{{cite web |title = agda-mode on Atom |url = https://atom.io/packages/agda-mode |access-date = 7 April 2017 }}</ref><ref>{{Cite web |title=agda-mode - Visual Studio Marketplace |url=https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode |access-date=2023-06-06 |website=marketplace.visualstudio.com |language=en-us}}</ref> but can also be run in batch mode from the command line.
Agda is based on Zhaohui Luo's unified theory of dependent types (UTT),<ref>Luo, Zhaohui. ''Computation and reasoning: a type theory for computer science''. Oxford University Press, Inc., 1994.</ref> a type theory similar to [[Intuitionistic type theory|Martin-Löf type theory]].
Agda is named after the [[Swedish language|Swedish]] song "Hönan Agda", written by [[Cornelis Vreeswijk]],<ref>{{cite web |title = [Agda] origin of "Agda"? (Agda mailing list)|url = https://lists.chalmers.se/pipermail/agda/2016/008867.html |access-date = 24 Oct 2020}}</ref> which is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the name of the theorem prover [[Coq (software)|Coq]], which was named after [[Thierry Coquand]], Catarina Coquand's husband.
== Features ==
Line 63:
=== Metavariables ===
One of the distinctive features of Agda, when compared with other similar systems such as [[Coq (software)|Coq]], is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:
<syntaxhighlight lang="agda">
| |||