<div dir="ltr">Hi Sergei,<div> You should probably read the <a href="https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html">documentation</a> for the `with` abstraction as it'll answer many of your questions. In particular it describes when `with` performs poorly and why `case` can't do everything `with` can.</div><div>Best,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Apr 11, 2019 at 7:01 AM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</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">Dear Agda team,<br>
<br>
Style guide  of standard library writes for the code committers that<br>
it is better to use the `with' construct than  case_of_. <br>
But<br>
<br>
(1) Earlier the team advised me to use case_of_ as possible.<br>
<br>
(2) I have a small application that adds a few items to standard     <br>
    library, and a certain function  f  in the end that type-checks in <br>
    5 seconds when f is written via case_of_ and its type check seems <br>
    to loop infinitely when f is written via `with'.<br>
<br>
Currently the Style guide actually suggests to use `with' everywhere<br>
where it type-checks reasonably fast, and to use case_of_ in other<br>
cases.<br>
<br>
Let a function  g  from standard be written via `with' and be<br>
type-checked fast. May it occur that when it is used in application, it<br>
explodes the type checking as in the example (2) ?<br>
<br>
Is not it better to use case_of_ instead of `with' in standard library<br>
everywhere where it is type-checked?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
_______________________________________________<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>