[Agda] The proving cycle.

[effectfully]

Hi. That's how I define a recursive function in Agda:

1) f : {A} -> B -> C -> D
    f y z = {!!}

2) Split on `y' or `z'. At this stage Agda often changes code
formatting and makes e.g.

    f : {A} -> B -> C -> D
    f {x} y z = {!!}

from

    f : {A} -> B -> C -> D
    f {x = x} y z = {!!}

I revert these changes.

3) Look at the context and the type of a term. Very often the context
and the term are not normalized, and I need to do this manually. Terms
usually contain implicit arguments, so C-c C-n doesn't work, and I
have to bind these implicits, again manually.

4) Remove stuff like (λ {.x} {.y} → ...).

5) When everything become explicit, I type C-c C-n and sometimes get
(_42 a dh dfh f sd). Agda doesn't display implicits in terms (as to
ShowImplicit: [1]), so it's sometimes impossible to meaningfully
normalize a term without additionally instantiating some implicits,
which can be non-trivial.

6) C-c C-r time. Agda again ignores my formatting, so I copy an
expression, refine the hole, delete the mess that Agda made from my
code (it sometimes even doesn't typecheck, especially when sections
are involved: Agda outputs something like (λ .section₀ → .section₀ +
m)) and paste the untouched expression.

When terms are large the whole process may take up to 20 minutes or
even more. Then I prove the theorem in 2 minutes.

Am I doing something wrong?

Here are some proposals:

1) The ability to normalize the type of a term in a context. The
ability to see the normalized type of a term in a hole (i.e. something
similar to C-c C-d or C-c C-., but with full normalization). The
ability to normalize a whole context.

2) Refine doesn't change formatting.

3) Something like C-c C-i makes an implicit explicit. I.e. C-c C-i i makes

i : I
x : A

from

.i : I
x : A

and inserts a lambda in the appropriate place.

4) More control on how things are evaluated. I rarely want `map' to be
unfolded into `replicate' and `_⊛_', but I always want `const', `_∘_',
`uncurry' and other combinators to be unfolded fully (which can
probably be a good heuristic on its own).

5) It would be nice, if it would be possible to declare fixities for
arguments. Maybe something like (infixl 6 _+_ : ℕ -> ℕ -> ℕ).

I realize that most of these proposals are fairly complex, but I hope
it's not just me being silly and there are other people that have
problems with using Agda, when complicated terms are involved. I'd
also appreciate if someone told me how to make the process of writing
code in Agda more straightforward.

Thanks for the attention.

[1] http://lpaste.net/138758