The Coq mailing list

[Xuanrui Qi <xuanrui AT nagoya-u.jp>]

> In Agda one can reuse names of fields in records, while in Coq that 
> yields an error

I'm not sure this is always desirable. Shadowing of field names can be
confusing at times so I'd not always call this a "usability
improvement".

Meanwhile, I do have my opinion on how Agda is better than Coq, but IMO
it's not due to the design of the theorem provers, but rather the fact
that Agda has more edit-time utilities and tool support. I'd like to
share my Coq Workshop 2019 slides (& accompanying abstract) where I
elaborate on the ergonomics of Coq programming: 

https://www.xuanruiqi.com/assets/coqws2019_long.pdf
https://www.xuanruiqi.com/assets/coqws2019_slides.pdf

-Xuanrui


On Fri, 2020-01-17 at 20:33 +0100, Sergey Goncharov wrote:
> On 17/01/2020 20:06, Agda Guru wrote:
> > Agda is better
> 
> This looks like a start of a new amusing thread. I am willing to
> believe 
> that Agda is better, but I would be happy if someone helps me to 
> rationalize this subtle feeling, in particular by going beyond this
> list 
> https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
> 
> Let me start. Foundational issues aside, Agda seems to be better 
> designed, as a programming language, in particular, as a recently
> learned:
> 
> 1. In Agda one can reuse names of fields in records, while in Coq
> that 
> yields an error:
> 
> Parameter X : Set.
> 
> Record some_record : Set :=
> {
>    field_name : X
> }.
> 
> Record some_other_record : Set :=
> {
>    field_name : X
> }.
> 
> ----> "Error: field_name already exists."
> 
> 
> Cheers,
>

Attachment: signature.asc
Description: This is a digitally signed message part