[Agda] `with' in standard functions

[Nils Anders Danielsson]

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.

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

-- 
/NAD