<div dir="ltr"><div>I recently had to move a local function to top-level. Previously I used irrelevance to to disregard the fact that I provide different (in name only) functions. I was lucky that the function did not use many local variables. <br><br></div>My main problem with 'with' is the error message. Someone on twitter said that "Type-driven development allows him to prove things that he wouldn't be able to do on his own".<br><br> When the complexity of the code increases, the 'with' error message does not increase our ability to handle that complexity. We have to solve things ourselves.<br><br><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 26, 2017 at 10:47 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2017-09-26 at 21:13 +0200, Nils Anders Danielsson wrote:<br>
> On 2017-09-26 20:09, Sergei Meshveliani wrote:<br>
> > Can you, please, demonstrate this parsing on a simple example?<br>
><br>
> Agda currently prints expressions of this form, but does not parse them.<br>
><br>
<br>
</span>I meant: how will it look the intended parsing result, for a simple<br>
example.<br>
<span class=""><br>
<br>
> > How would this  aux  be referred from outside?<br>
><br>
> Let's take the following, self-contained example instead:<br>
><br>
>    open import Agda.Builtin.List<br>
>    open import Agda.Builtin.Nat<br>
><br>
>    F : List Set → Set<br>
>    F []       = Nat<br>
>    F (A ∷ As) = B 12<br>
>      module M where<br>
>      B : Nat → Set<br>
>      B zero    = A<br>
>      B (suc n) = A → B n<br>
><br>
> Here you can refer to the local function B as M.B. Note, however, that<br>
> the inferred type of M.B is (A : Set) (As : List Set) → Nat → Set. In<br>
> cases like this, where one or more arguments are not used by the local<br>
> function and you want to refer to it by name, it may be better to move<br>
> it to the top-level than to name the where module.<br>
><br>
<br>
</span>Year or two ago I tried this once. And decided that it is still better<br>
to move it to the top level, even with polluting the top level with<br>
"-aux" functions.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>