Talk:Agda (programming language)

Latest comment: 1 year ago by 58.96.219.177 in topic Cubical type theory support

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 (talkcontribs) 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

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)Reply