[Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker

[Nils Anders Danielsson]

On 2013-09-17 15:09, Sergei Meshveliani wrote:
> But I need a general understanding:  when to use `with' and when to
> use `case'.

When you use with Agda creates a helper function. As part of the
creation of this function Agda performs the following steps:

* Normalise the context and goal type.

* For each term that you abstract over: Normalise the term, find all
   syntactic occurrences of the normal form in the (normalised) context
   and goal type, and replace these occurrences by a fresh variable.

These steps can be expensive.

-- 
/NAD