Content deleted Content added
No edit summary |
Matt Crypto (talk | contribs) Image is decorative, rather than illustrative; it'd be much better to give actual examples in text |
||
Line 20:
| operating_system = [[Cross-platform]]
}}
'''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]].
| |||