We have two ways of looking up statements in RTLabs:
- lookup, which returns an option type, and
- lookup_present, which uses a proof that the label exists (defined in terms
of lookup).
Occasionally we end up with one when we want the other, or two lookup_present
terms with different proofs, but we can deal with these. The bigger problem
is that we have two ways of talking about successors:
- label_P asserts a predicate on each label in a statement, and
- successors returns a list of labels.
We've used the former in the transformations, but recently I've used the latter
in the structured traces and the two are conflicting a little. Attempting to
rewrite a recent inductive type in terms of label_P reveals a positivity
problem.
A little more prodding showed that this wasn't really much of a problem, so I'll
leave it aside for now.