Changeset 1317 for Deliverables/D3.2/Report

Timestamp:

Oct 7, 2011, 12:28:46 PM (9 years ago)

Author:

campbell

Message:

Fix listings in D3.2/D3.3.

File:

• Deliverables/D3.2/Report/report.tex (modified) (3 diffs)

Deliverables/D3.2/Report/report.tex

@@ -365 +365 @@
 record internal_function : Type[0] ≝
 { f_return    : option typ
-; f_params    : list (ident × typ)
-; f_vars      : list (ident × typ)
+; f_params    : list (ident $\times$ typ)
+; f_vars      : list (ident $\times$ typ)
 ; f_stacksize : nat
 ; f_body      : stmt
-; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
-                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
+; f_inv       : stmt_P ($\lambda$s.stmt_vars ($\lambda$i.Exists ? ($\lambda$x.\fst x = i) (f_params @ f_vars)) s $\wedge$
+                           stmt_labels ($\lambda$l.Exists ? ($\lambda$l'.l' = l) (labels_of f_body)) s) f_body
 }.
 \end{lstlisting}
@@ -383 +383 @@
                    (Env:expr_vars ty e (present ?? env))
                    (dst:register) (f:partial_fn le) on e
-     : Σf':partial_fn le. fn_graph_included le f f' ≝
-match e return λty,e.expr_vars ty e (present ?? env) →
-                 Σf':partial_fn le. fn_graph_included le f f' with
-[ Id _ i ⇒ λEnv.
+     : $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝
+match e return $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$
+                 $\Sigma$f':partial_fn le. fn_graph_included le f f' with
+[ Id _ i $\Rightarrow$ $\lambda$Env.
     let r ≝ lookup_reg env i Env in
     ...
@@ -400 +400 @@
 on variables needed by \lstinline'add_expr' and its equivalent on statements:
 \begin{lstlisting}[language=matita]
-lemma populates_env : ∀l,e,u,l',e',u'.
-  populate_env e u l = 〈l',e',u'〉 →
-  ∀i. Exists ? (λx.\fst x = i) l →
+lemma populates_env : $\forall$l,e,u,l',e',u'.
+  populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$
+  $\forall$i. Exists ? ($\lambda$x.\fst x = i) l $\rightarrow$
       present ?? e' i.
 \end{lstlisting}