Talk:Agda (programming language)
| This is the talk page for discussing improvements to the Agda (programming language) article. This is not a forum for general discussion of the article's subject. |
Article policies
|
| Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||
| |||||||||||||||||
.svg){kind=logo}
Untitled edit
I would love to see the constructor z<=n clarified with an example of its use: hard to understand the meaning if you don't already know the syntax details of Agda: is "z" a parameter of the constructor? Is "n" a parameter? Is "n" the only parameter? Is "z" a symbolic constant? — Preceding unsigned comment added by Rebcabin (talk • contribs) 14:14, 25 January 2015 (UTC)
I tried to clean up this page but my change was reverted. The information that is there is misleading and inaccurate. I copied the text from the agda wiki which I thought was better. What copyright do we need to use for the agda wiki to make it compatible with wikipedia? And what would it take to get my changes approved? — Preceding unsigned comment added by 130.226.142.226 (talk) 15:44, 8 October 2012 (UTC)
I suspect I'm not going to get an answer here so I will take a more conservative approach and try to fix the problems instead of replacing the text with the wiki text. — Preceding unsigned comment added by 130.226.142.226 (talk) 09:27, 9 October 2012 (UTC)
As someone new to Agda who stumbled across the wikipedia page, it may be helpful to define what suc means in these examples? After digging through some links I'm assuming it's the Successor_function ? anon. 162.213.148.250 (talk) 19:04, 23 May 2017 (UTC)
Cubical type theory support edit
I think a worthwhile addition would be a paragraph on Agda's cubical features, as one of the few preexisting mature languages that got CTT retrofitted. 58.96.219.177 (talk) 05:28, 27 June 2023 (UTC)