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

All times shown according to UTC.

Time Nick Message
09:23 kowey joined #darcs-theory
09:55 Heffalump joined #darcs-theory
13:29 gal_bolle joined #darcs-theory
13:30 gal_bolle hi all
13:30 gal_bolle hi Igloo
13:30 gal_bolle the first one is with definition 8.5
13:31 gal_bolle isn't there a positive way of stating it?
13:33 gal_bolle something like:
13:33 gal_bolle Given two sequences ending with two patches with the same name n,
13:33 gal_bolle we can commute them into a common part ending with a patch with name
13:33 Igloo gal_bolle: You mean "names-global"?
13:33 gal_bolle n, and the rest of each. That is, we can get back to the context in
13:33 gal_bolle which a patch named n was first recorded, except for patches which
13:33 gal_bolle were unpulled in either s or s'.
13:33 gal_bolle yes
13:33 gal_bolle i'm trying to teach coq how to deal with patches, and it does not like at all definition 8.5
13:34 gal_bolle (the concept of fresh names is quite hard to formalise)
13:36 gal_bolle the second problem is with the definition of contexted-patch: what happens if p^ is hidden further inside q than just the first element?
13:38 Igloo For the second problem, you'd commute the sequence first (and then commute back afterwards if you want)
13:39 gal_bolle so the \neq really reads "can't be commuted into p^q' "
13:40 Igloo Which \neq?
13:40 gal_bolle q ≠ p^q'
13:45 Igloo I've just made sure I have the latest thing built, and I don't see that in 8.5
13:46 Igloo Oh, sorry
13:46 gal_bolle in 8.5 i'm only complaining about the fact that fresh names don't make good proof arguments
13:47 gal_bolle the paper is definitely making progress though, that's really awesome
13:48 Igloo OK, yes, the \neq really reads "can't be commuted into p^q' "
13:48 Igloo And yes, I'll think about the fresh name thing some more
13:58 kowey joined #darcs-theory
19:21 arjanb joined #darcs-theory
22:26 kowey joined #darcs-theory