the information needed to construct the boolean proposition that encods the equality proposition (V = C)
the information needed to construct the boolean proposition that encods the equality proposition (V = C)
that models a type test pattern _: C
or constant pattern C
, where the type test gives rise to a TypeConst C,
and the constant pattern yields a ValueConst C
for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match, and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1"