<div dir="ltr"><div>Hi Joey,</div><div><br></div><div>The note that it is experimental mainly refers to the fact that there is no proper solver yet for level (in)equalities, so there will be (possibly quite frequent) cases where you have to fill in implicit level arguments that Agda is able to infer without --cumulativity. That being said, it is also a new feature in Agda and it hasn't been tested very extensively yet so there may also still be bugs of the "make Agda unsound" kind. Running Agda with the --double-check flag enabled might catch some of these bugs when they occur.</div><div><br></div><div>-- Jesper</div><div><br></div><div>ps: If anyone is interested in implementing a proper solver for universe levels, please get in touch! There may be some interesting research questions lurking there.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jan 3, 2020 at 8:28 PM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com">joey.eremondi@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto">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?<div dir="auto"><br></div><div dir="auto">Thanks!</div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>