-
Notifications
You must be signed in to change notification settings - Fork 226
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
written
type is inp2
, andwritten <: provisionalType
, then
newPromotionChain
is[...promotionChain, written]
. ...- Otherwise (when
written
is 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