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