|
@@ -187,8 +187,9 @@ We want the type $\{f : T\}$ to express \enquote{any record with a field $f$ of
|
|
|
To do this, we introduce the following sub-typing relation:
|
|
|
|
|
|
\[
|
|
|
- \inference{}{\{f_1 : T_1; \dots f_n : T_n; g_1 : S_1; \dots ; g_k : S_k\} <: \{f_1 : T_1; \dots f_n : T_n\}}
|
|
|
+ \inference{}{\{f_1 : T_1; \dots ; f_n : T_n; g_1 : S_1; \dots ; g_k : S_k\} <: \{f_1 : T_1; \dots ; f_n : T_n\}}
|
|
|
\]
|
|
|
+% FIXME on avait noté la relation <: dans l'autre sens
|
|
|
|
|
|
Note that in order to assure the reflexivity of our relation,
|
|
|
a type $S$ is a sub-type of $T$ if all the fields of $T$ are included in $S$.
|