IRC log for #darcs-theory, 2009-04-03

All times shown according to UTC.

Time Nick Message
03:46 arjanb joined #darcs-theory
09:45 gal_bolle joined #darcs-theory
11:41 gal_bolle i'll finish modulizing my coq
11:42 Igloo OK; I switched to modules too, and now no more Notation duplication; woo  :-)
11:43 gal_bolle cool
11:43 gal_bolle we're starting to see some convergence between our solutions, that's nice
11:44 Igloo Yup
11:47 gal_bolle looking at sensible sequences again, do you want the axiom if p:>s is sensible, then so is s?
11:47 gal_bolle ie: are your sensible sequences grounded?
11:48 Igloo sensible sequences always start from the empty repo
11:49 gal_bolle ok, then i'd introduce quasi-sensible sequences (tactful sequences?) which do not have that constraint
11:49 Igloo Why are they useful?
11:50 gal_bolle so that we can show that there is a set of states such that each (unnamed) patch goes from one state to another, and a sequence is sensible if states correspond
11:50 Igloo If X is quasi-sensible and Y is quasi-sensible then X;Y might not be
11:50 gal_bolle no, you need an intermediary p
11:50 gal_bolle if sp and ps' are quasi-sensible, then so is sps'
11:50 gal_bolle that's
11:50 gal_bolle what i wanted to have
11:51 gal_bolle so that you need only to look at one patch to know that the sequence is quasi-sensible
11:51 Igloo OK
11:52 gal_bolle i really prefer patches with witness states to sensibility
11:53 gal_bolle so i wanted to prove they were equivalent
11:54 Igloo Hmm, yes, I think you are right
12:00 gal_bolle what i don't know is how hints behave with respect to module boundaries
12:00 gal_bolle i'll have to look that up
16:48 gal_bolle joined #darcs-theory
16:51 arjanb joined #darcs-theory
16:58 jnaimard joined #darcs-theory