Agda (programming language): Difference between revisions

Revision as of 19:31, 31 October 2021

Revision as of 04:07, 31 December 2021

Line 3:

| name = Agda

| logo = Agda's official logo.svg

| logo alt = A stylized chicken in black lines and dots, to the left of the name “Agda”"Agda" in sans-serif test with the first letter slanted to the right.

| paradigm = [[functional programming|Functional]]

| year = {{Start date and age|2007}} (1.0 in {{Start date and age|1999}})

Line 43:

suc : ℕ → ℕ

</syntaxhighlight>

Basically, it means that there are two ways to construct a value of type ℕ<math>\mathbb{N}</math>, representing a natural number. To begin, <code>zero</code> is a natural number, and if <code>n</code> is a natural number, then <code>suc n</code>, standing for the [[Successor function|successor]] of <code>n</code>, is a natural number too.

Here is a definition of the "less than or equal" relation between two natural numbers:

Line 85:

</syntaxhighlight>

Given a function <code>check-even : (n : ℕ<math>\mathbb{N}</math>) → Maybe (Even n)</code> that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows:

<syntaxhighlight lang="agda">

Line 135:

* [http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf A Brief Overview of Agda], by Ana Bove, Peter Dybjer, and [[Ulf Norell]]

* [https://www.youtube.com/playlist?p=B7F836675DCE009C Introduction to Agda], a five-part YouTube playlist by Daniel Peebles

* [http://oxij.org/note/BrutalDepTypes/ Brutal &#91;{{bracket|Meta&#93;}}Introduction to Dependent Types in Agda]

* [http://people.inf.elte.hu/divip/AgdaTutorial/Index.html Agda Tutorial: "explore programming in Agda without theoretical background"]