[Agda] `with' in standard functions

[Sergei Meshveliani]

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