[Agda] A puzzle with "with"
Ana Bove
bove at chalmers.se
Thu Jun 25 18:40:43 CEST 2009
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
************************************************************************
More information about the Agda
mailing list