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.

Put new text under old text. Click here to start a new topic.
New to Wikipedia? Welcome! Learn to edit; get help.

Article policies

Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL

Computing: Software / Free and open-source software

	This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing articles
???	This article has not yet received a rating on the project's importance scale.
	This article is supported by WikiProject Software.
	This article is supported by Free and open-source software (assessed as Low-importance).

Untitled

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)[reply]

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)[reply]

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)[reply]

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)[reply]

Cubical type theory support

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)[reply]