Content deleted Content added
Mention of emacs mode and of epigram |
Removed {{context}} warning and changed a bit the introduction |
||
Line 1:
[[Image:Agda_proof.jpg|thumb|300px|right|Excerpt of a proof in '''agda2''']]
'''Agda''' is a theorem prover, i.e. a computer program that can check mathematical proofs. More specifically, it 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.
| |||