[Agda] `with' in standard functions

[Nils Anders Danielsson]

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

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

-- 
/NAD