Sub-range inclusion
<=
\ffrac{
n <= n'
and
m' <= m
}{
n'..m' <= n..m
}
Functions
contravariance
\ffrac{
%s <= %s'
and
%t' <= %t
}{
%s' -> %t' <= %s -> %t
}
Records
\ffrac{
%s_i <= %t_i
for
i = 1..m
(
m <= n
) }{
{a_1: %s_1, ... , a_n: %s_n} <= {a_1: %t_1 , ... , a_m: %t_m}
}
Variants
\ffrac{
%s_i <= %t_i
for
i = 1..m
(
m <= n
) }{
[a_1:%s_1 \/ ... \/ a_m:%s_m] <= [a_1:%t_1 \/ ... \/ a_n:%t_n]
}
slide
:
The subtype refinement relation
