Content deleted Content added
Matt Crypto (talk | contribs) Image is decorative, rather than illustrative; it'd be much better to give actual examples in text |
Undid revision 322618365 by Matt Crypto (talk) don't see any reason not to use it. removing it won't magically make examples appear |
||
Line 20:
| operating_system = [[Cross-platform]]
}}
[[Image:Agda proof.jpg|thumb|300px|right|Excerpt of a proof in '''agda2''']]
'''Agda''' is a [[proof assistant]], 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 by [[Ulf Norell]], a post-doc at [[Chalmers University of Technology]].
| |||