Définition du domaine des opérateurs o

dm.tex

@@ -69,7 +69,7 @@ where
 \begin{align*}
   \mathcal{A} |[ n |] \sigma &= \mathcal{N} |[n|] \\
   \mathcal{A} |[ x |] \sigma &= \sigma x \\
-  \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma \\
+  \mathcal{A} |[ e_1\ o\ e_2 |] \sigma &= \mathcal{A} |[ e_1 |] \sigma\ \bar{o}\ \mathcal{A} |[ e_2 |] \sigma, o \in \{+, -, \times\} \\
   \mathcal{A} |[ e.f |] \sigma &= \mathcal{A}|[e|] \sigma f\\
   \mathcal{A} |[ e_1{f \mapsto e_2} |] \sigma f &= \mathcal{A}|[ e_1 |] \sigma [f \mapsto \mathcal{A}|[ e_2 |] \sigma ]\\
   \mathcal{A} |[ \{f_1 = e_1 ; \dots ; f_n = e_n\} |] \sigma f_i &= \mathcal{A}|[ e_i |] \sigma \\
@@ -155,7 +155,7 @@ We note $\Gamma \vdash S$ the type judgment for our language, defined by the fol
   \inference{(x : T) \in \Gamma}{\Gamma \vdash x : T}
 \]
 \[
-  \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1\ o\ a_2 : int}
+  \inference{\Gamma \vdash a_1 : int & \Gamma \vdash a_2 : int}{\Gamma \vdash a_1\ o\ a_2 : int}{o \in \{+, -, \times\}}
 \]
 
 Records