Idris2 + extensible records/row polymorphism/anonymous records ?

84 views
Skip to first unread message

Jeremy Shaw

unread,
May 19, 2022, 10:41:55 AM5/19/22
to idris...@googlegroups.com
Ahoy!

I am looking for a library which supports adhoc, extensible, anonymous records. Something like these Idris 1 libraries:

Has anything been created for Idris2 already? Or should I try porting the existing libraries from Idris1 to Idris2?

Also, is anyone thinking of adding native extensible record support in Idris2? I am not really sure what advantages I would expect -- perhaps just cleaner syntax.

Thanks!

- jeremy
Reply all
Reply to author
Forward
0 new messages