Member predicate MakeWithSplitting::SplitImpl::hasSuccessor
Holds if this split is maintained when control passes from pred
to succ
with
completion c
.
Invariant: hasSuccessor(pred, succ, c) implies succ(pred, succ, c)
predicate hasSuccessor(AstNode pred, AstNode succ, Completion c)