[Agda] How experimental is Cumulativity?

[Joey Eremondi]

I see that Cumulativity is listed as an experimental feature in 2.6.1. Is
this "the compiler might crash or reject valid programs" experimental? Or
"Cumulativity might make Agda unsound" experimental? How much can I trust
proofs that use cumulative Agda?

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200103/7fb44cf3/attachment.html>