Changeset 1317 for Deliverables/D3.2


Ignore:
Timestamp:
Oct 7, 2011, 12:28:46 PM (8 years ago)
Author:
campbell
Message:

Fix listings in D3.2/D3.3.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.2/Report/report.tex

    r1277 r1317  
    365365record internal_function : Type[0] ≝
    366366{ f_return    : option typ
    367 ; f_params    : list (ident × typ)
    368 ; f_vars      : list (ident × typ)
     367; f_params    : list (ident $\times$ typ)
     368; f_vars      : list (ident $\times$ typ)
    369369; f_stacksize : nat
    370370; f_body      : stmt
    371 ; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
    372                            stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
     371; f_inv       : stmt_P ($\lambda$s.stmt_vars ($\lambda$i.Exists ? ($\lambda$x.\fst x = i) (f_params @ f_vars)) s $\wedge$
     372                           stmt_labels ($\lambda$l.Exists ? ($\lambda$l'.l' = l) (labels_of f_body)) s) f_body
    373373}.
    374374\end{lstlisting}
     
    383383                   (Env:expr_vars ty e (present ?? env))
    384384                   (dst:register) (f:partial_fn le) on e
    385      : Σf':partial_fn le. fn_graph_included le f f' ≝
    386 match e return λty,e.expr_vars ty e (present ?? env) →
    387                  Σf':partial_fn le. fn_graph_included le f f' with
    388 [ Id _ i ⇒ λEnv.
     385     : $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝
     386match e return $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$
     387                 $\Sigma$f':partial_fn le. fn_graph_included le f f' with
     388[ Id _ i $\Rightarrow$ $\lambda$Env.
    389389    let r ≝ lookup_reg env i Env in
    390390    ...
     
    400400on variables needed by \lstinline'add_expr' and its equivalent on statements:
    401401\begin{lstlisting}[language=matita]
    402 lemma populates_env : l,e,u,l',e',u'.
    403   populate_env e u l = 〈l',e',u'〉 →
    404   ∀i. Exists ? (λx.\fst x = i) l →
     402lemma populates_env : $\forall$l,e,u,l',e',u'.
     403  populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$
     404  $\forall$i. Exists ? ($\lambda$x.\fst x = i) l $\rightarrow$
    405405      present ?? e' i.
    406406\end{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.