[Agda] `with' in standard functions

[Apostolis Xekoukoulotakis]

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.

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".

 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.



On Tue, Sep 26, 2017 at 10:47 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Tue, 2017-09-26 at 21:13 +0200, Nils Anders Danielsson wrote:
> > On 2017-09-26 20:09, Sergei Meshveliani wrote:
> > > Can you, please, demonstrate this parsing on a simple example?
> >
> > Agda currently prints expressions of this form, but does not parse them.
> >
>
> I meant: how will it look the intended parsing result, for a simple
> example.
>
>
> > > How would this  aux  be referred from outside?
> >
> > Let's take the following, self-contained example instead:
> >
> >    open import Agda.Builtin.List
> >    open import Agda.Builtin.Nat
> >
> >    F : List Set → Set
> >    F []       = Nat
> >    F (A ∷ As) = B 12
> >      module M where
> >      B : Nat → Set
> >      B zero    = A
> >      B (suc n) = A → B n
> >
> > Here you can refer to the local function B as M.B. Note, however, that
> > the inferred type of M.B is (A : Set) (As : List Set) → Nat → Set. In
> > cases like this, where one or more arguments are not used by the local
> > function and you want to refer to it by name, it may be better to move
> > it to the top-level than to name the where module.
> >
>
> Year or two ago I tried this once. And decided that it is still better
> to move it to the top level, even with polluting the top level with
> "-aux" functions.
>
> Regards,
>
> ------
> 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/20170927/802ae1cb/attachment.html>