[Agda] `with' vs `case'

[Matthew Daggitt]

Hi Sergei,
 You should probably read the documentation
<https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html> 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.
Best,
Matthew

On Thu, Apr 11, 2019 at 7:01 AM Sergei Meshveliani <mechvel at botik.ru> wrote:

> Dear Agda team,
>
> Style guide  of standard library writes for the code committers that
> it is better to use the `with' construct than  case_of_.
> But
>
> (1) Earlier the team advised me to use case_of_ as possible.
>
> (2) I have a small application that adds a few items to standard
>     library, and a certain function  f  in the end that type-checks in
>     5 seconds when f is written via case_of_ and its type check seems
>     to loop infinitely when f is written via `with'.
>
> Currently the Style guide actually suggests to use `with' everywhere
> where it type-checks reasonably fast, and to use case_of_ in other
> cases.
>
> Let a function  g  from standard be written via `with' and be
> type-checked fast. May it occur that when it is used in application, it
> explodes the type checking as in the example (2) ?
>
> Is not it better to use case_of_ instead of `with' in standard library
> everywhere where it is type-checked?
>
> Thanks,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190411/310b8e8f/attachment.html>