-
Notifications
You must be signed in to change notification settings - Fork 227
Open
Labels
flow-analysisDiscussions about possible future improvements to flow analysisDiscussions about possible future improvements to flow analysisspecification
Description
The flow-analysis definition of toi_promote has the following:
toi_promote(declared, promotionChain, tested, written), where ...
...
- If the
writtentype is inp2, andwritten <: provisionalType, then
newPromotionChainis[...promotionChain, written]. ...- Otherwise (when
writtenis not inp2):
This is somewhat confusing to read because it seems to skip over the case where written is in p2, but written <: provisionalType does not hold.
However, written <: provisionalType is guaranteed to hold in all cases because of the preconditions which are specified in order to use toi_promote (and because the only "call site" for toi_promote is known to satisfy those preconditions).
Granted, this is a request for a tiny change, but I do think the rule will be easier to read if "and written <: provisionalType" is removed, or it is changed to commentary.
Metadata
Metadata
Assignees
Labels
flow-analysisDiscussions about possible future improvements to flow analysisDiscussions about possible future improvements to flow analysisspecification