Idris2 + extensible records/row polymorphism/anonymous records ?

[Jeremy Shaw]

Ahoy!

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

https://github.com/gonzaw/extensible-records

https://github.com/berewt/flexidisc

Or this Haskell library:

https://hackage.haskell.org/package/bookkeeper-0.2.5/docs/Bookkeeper.html

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