[Agda] A puzzle with "with"

[Ana Bove]

Hi,

I must say I am confuse as well....

let us simply consider the case were we want to insert x in (y :: ys)
and comp x y = Lt

Then the insert function simply returns x :: y :: ys and in that eq. of
the sorted-insert we need to simply give a proof that Sorted (x :: y :: ys).

Now, if in this equation I write

......
sorted-insert x (y ∷ ys) prf with Order.comp o x y
sorted-insert x (y ∷ ys) prf | Lt =
let q : Sorted (x ∷ y ∷ ys)
q = ?
in q
......

then I can type check.

However, if I try to do the same in the sorted-insert2 it does not!

......
sorted-insert2 x (y ∷ ys) prf with inspect (Order.comp o x y)
sorted-insert2 x (y ∷ ys) prf | Lt with-≡ p =
let q : Sorted (x ∷ y ∷ ys)
q = ?
in q
......

I get the error

x ∷ y ∷ ys != insert x (y ∷ ys) | Order.comp o x y of type List A
when checking that the expression q has type
Sorted (insert x (y ∷ ys) | Order.comp o x y)

q should be the term
sorted-cons2 x y ys prf (biimply-fwd (Order.isLtComp o x y) (symm p))
(well, the whole let of course should not be used)

And I must say I do not understand why. I never used inspect before but
I thought the difference with inspect was that not only gave me the
result I would get without inspect but also the "evidence" of that result.
But otherwise it should not matter.

Best

-- 
-- Ana

************************************************************************
                                ANA  BOVE
bove(at)chalmers.se     Department of Computer Science and Engineering
http://www.cse.chalmers.se/~bove     Chalmers University of Technology
Phone (work) :(46)(31) 772 10 20          and University of Gothenburg
Fax (work)   :(46)(31) 772 36 63        S-412 96 Gothenburg  -  SWEDEN
************************************************************************