[Agda] `with' --> `case' fails

[Sergei Meshveliani]

On Fri, 2013-09-27 at 14:24 -0400, Andreas Abel wrote:

> The full code would be helpful to answer your question. --Andreas


Today I reported the simplified code to the Bug tracker 
(the archive with  Power.agda  and readme.agda).

A 2/3 page program, it is a full code, and very simple.
`readme' asks:  
         how to reduce the repeated code block in the `with' branches?  

Thanks,

------
Sergei

> On 26.09.2013 13:29, Sergei Meshveliani wrote:
> > Please how to rewrite the `with' program to the `case' one in the below
> > example?
> >
> > The `with' variant has repetitions (of the  pp∙x=x∙pp  implementation
> > and others) in the two `with' branches. These unpleasant repetitions
> > must (as I think) disappear in the `case' version.
> >
> > The `with' version is type-cheked.
> > But my `case' version (obtained by the most natural conversion) is not.
> > [..]