Agda records are not as nice as Lean structures, huh? Or am I missing something?
Conversation
I can model "extends" by just making a field for the super record, but then accessing its fields becomes extra inconvenient.
Am I supposed to do this differently?
1
4
This Tweet was deleted by the Tweet author. Learn more
Thanks! What do people do in practise with these sorts of hierarchies? In Lean I've got a structure with three fields and then a parameterised structure that "adds a fourth" and it inserts coercions automatically from the latter to the former.
2
2
I think I remember seeing `{{field}}` but I think you need to use instance args to get it to look through that path?
1
2
Those are sort-of typeclasses, but Agda has strong restrictions over them...
1
2
Yeah, they seem pretty neat, but I’ve never used them in practice. I’ve also seen people `open`ing fields, but that’s about it 🤔