[Agda] Re: problem using "with"

[Guillermo Calderón]

On 15/05/12 05:58, Nils Anders Danielsson wrote:
> On 2012-05-14 17:50, Guillermo Calderón wrote:
>> From your explanations, I do understand how the "with" works.
>> But this behaviour results rather counter-intuitive to me.
>
> What kind of behaviour would be intuitive, if any?
>


I would expect that the type checker could proceed this way

(1) -  (f2 n p)  has type R (g n)
(2) -  (g n)  reduces to n  when (n ≤? 5) matchs (yes p)

then
          (f2 n p) has type (R n)

But Agda  does not take  account of (2)  to infer the type of the right 
hand side.

As a naive user, I would expect  that the particular case of the "with"
took effect also on the right hand side of the equation.