[Agda] `with' in standard functions

[Nils Anders Danielsson]

On 2017-09-26 21:47, Sergei Meshveliani wrote:
> I meant: how will it look the intended parsing result, for a simple
> example.

Consider the following code:

   f : {A : Set} → List A → List A
   f []       = []
   f (x ∷ xs) with xs
   ... | []     = xs
   ... | y ∷ ys = x ∷ ys

This is expanded into something like the following:

   .f-aux : {A : Set} → A → List A → List A → List A
   .f-aux x xs []       = xs
   .f-aux x xs (y ∷ ys) = x ∷ ys

   f : {A : Set} → List A → List A
   f []       = []
   f (x ∷ xs) = .f-aux x xs xs

The idea is that the expression f (x ∷ xs) | ys would stand for
.f-aux x xs ys.

-- 
/NAD