Content deleted Content added
m moved Agda theorem prover to Agda (theorem prover): Wikipedia:Disambiguation suggests parentheses for disambiguation. |
m Agda was developed at Chalmers University of Technology. |
||
Line 1:
{{context}}
'''Agda''' is an [[Interactive theorem proving|interactive system]] for developing [[constructive proof]]s in a variant of [[Per Martin-Löf]]'s [[Intuitionistic Type Theory|Type Theory]]. It can also be seen as a [[functional programming language]] with [[dependent type]]s and was developed at [[Chalmers University of Technology]].
Agda is based on the idea of direct manipulation of proof-term and not on tactics. The proof is a term, not a script. The language has ordinary programming constructs such as data-types and case-expressions, signatures and records, let-expressions and modules. The system has an [[emacs]]-interface and a [[graphical interface]], Alfa.
| |||