Time 
Nick 
Message 
03:46 

arjanb joined #darcstheory 
09:45 

gal_bolle joined #darcstheory 
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 quasisensible 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 quasisensible and Y is quasisensible 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 quasisensible, 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 quasisensible 
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 #darcstheory 
16:51 

arjanb joined #darcstheory 
16:58 

jnaimard joined #darcstheory 