[Agda] With and the inspect idiom

[Shin-Cheng Mu]

On May 11, 2008, at 11:19 PM, Ulf Norell wrote:
> Rather than resorting to transitivity lemmas you can pattern match =20
> on the
> first (or second) proof:
>
>  foo <something else> with inspect (f b)
>  foo <something else> | v with-=A1=DD v=A1=DDfb    with f b | v=A1=DDfb
>  foo <something else> | .(f b) with-=20
> =A1=DD =A1=DD-refl | (c , d) | fb=A1=DDcd =3D { }0
>
> Now fb=A1=DDcd : f b =A1=DD (c , d) which is =20
> exactly what we wanted. That's as simple
> as I can manage I'm afraid...

Thanks! It looks like a nice solution.

However, I am not sure I understand how it works. It seems that before
"with f b", v=A1=DDfb has type v =A1=DD fb. I =20
suppose that after the second "with",
Agda somehow know that it v equals f b, therefore v=A1=DDfb also has =
type
f b =A1=DD f b and may thus be matched with =20
=A1=DD-refl. But how did that happen?

And how come v=A1=DDfb also has type f b =A1=DD (c , d) in the last =
pattern?

sincerely,
Shin