Last change
on this file was
2394,
checked in by campbell, 7 years ago

I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.

File size:
860 bytes

Line  

1  We have two ways of looking up statements in RTLabs: 

2  

3   lookup, which returns an option type, and 

4   lookup_present, which uses a proof that the label exists (defined in terms 

5  of lookup). 

6  

7  Occasionally we end up with one when we want the other, or two lookup_present 

8  terms with different proofs, but we can deal with these. The bigger problem 

9  is that we have two ways of talking about successors: 

10  

11   label_P asserts a predicate on each label in a statement, and 

12   successors returns a list of labels. 

13  

14  We've used the former in the transformations, but recently I've used the latter 

15  in the structured traces and the two are conflicting a little. Attempting to 

16  rewrite a recent inductive type in terms of label_P reveals a positivity 

17  problem. 

18  

19  A little more prodding showed that this wasn't really much of a problem, so I'll 

20  leave it aside for now. 

Note: See
TracBrowser
for help on using the repository browser.