Camelia, the Perl 6 bug

IRC log for #darcs-theory, 2008-11-25

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
09:11 kowey joined #darcs-theory
15:58 kowey joined #darcs-theory
17:28 arjanb joined #darcs-theory
19:45 arjanb Igloo: theory.pdf on the camp website seems to be 2 months out of date
19:47 Igloo Thanks for the prod, updated
19:47 Igloo And I've made a Makefile target to make updating easier, so hopefully I'll do more of it  :-)
20:24 arjanb nice progress
20:24 Igloo Thanks!
20:25 arjanb for lemma 9.2 what about: minimal context of P is the common subset of N(Rs) for all Rs in QsP <-*-> RsP'Ts
20:27 Igloo What we need to prove is that is if   As P Bs <->* Cs P' Ds
20:28 Igloo Then we can commute out anything in As but not Cs, and vice-versa
20:29 Igloo Or to put it another way, if    As B Cs P Ds <->* Es P' Fs   where B \notin Es
20:29 Igloo Then <B, Cs P> <-> <Cs' P'', B'>
20:30 Igloo Which I think you can prove by considering the rightmost B, and using the previous lemma for each patch in Cs P. Does that sound good?
20:31 arjanb yeah
20:32 arjanb or it's just a matter of enumerating the ways of how B could have ended up in that place
20:33 Igloo I need to talk to gal_bolle about whether he can make coq happy with this approach
21:06 Heffalump gal_bolle is coq'ing stuff?
21:09 Igloo Yup
21:29 kowey joined #darcs-theory

| Channels | #darcs-theory index | Today | | Search | Google Search | Plain-Text | summary