source: etc/campbell/dev-notes/2012-02-16-labels-present.txt

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 
1We 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
7Occasionally we end up with one when we want the other, or two lookup_present
8terms with different proofs, but we can deal with these.  The bigger problem
9is 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
14We've used the former in the transformations, but recently I've used the latter
15in the structured traces and the two are conflicting a little.  Attempting to
16rewrite a recent inductive type in terms of label_P reveals a positivity
17problem.
18
19A little more prodding showed that this wasn't really much of a problem, so I'll
20leave it aside for now.
Note: See TracBrowser for help on using the repository browser.