[Agda] `with' in standard functions

[Sergei Meshveliani]

On Tue, 2017-09-26 at 10:27 +0200, Nils Anders Danielsson wrote:
> On 2017-09-24 13:46, Sergei Meshveliani wrote:
> > There is a certain problem with user proofs for Standard library
> > functions that use `with' or `case_of_'.
> 
> I guess that the main problem is when one or more parts of the first
> definition cannot be referred to directly in the second definition. Some
> examples:
> 
> * With. When with is used there is no way to refer directly (without
>    using unification) to the generated with function. We could perhaps
>    fix this by parsing with expressions of the form
>    "f ps | e_1 | ... | e_n".

Can you, please, demonstrate this parsing on a simple example? 
Say, on Data.Bin.fromBits.
?


> * Pattern-matching lambdas. Such lambdas are compared by name, but the
>    name is generated and cannot be written down explicitly in source
>    code. This could perhaps be fixed by comparing such lambdas by
>    structure rather than name, but that is a rather big change.
> 
> * Local definitions in where clauses. Such definitions are presumably
>    supposed to be hidden, but can be named if the where clause is named.

For example,  Data.Bin.fromBits  can be written as

fromBits : List Bit → Bin
fromBits []       = 0#
fromBits (b ∷ bs) = aux b bs (fromBits' bs)
              where
              aux : Bit → Bin → Bin  
              aux b  (bs' 1#) = (b ∷ bs') 1#
              aux 0b 0#       = 0#
              aux 1b 0#       = [] 1#
              aux ⊥b _

How would this  aux  be referred from outside?
("fromBits.aux" does not look as concrete enough).

Thanks,

------
Sergei