Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (7 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/extraGlobalenvs.ma

    r2570 r2590  
    2121    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
    2222    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b.
    23 *)
    2423
    2524definition is_function ≝ λF.λge : genv_t F.
     
    4746| None ⇒ λ_.None ?
    4847] (refl …).
     48*)
    4949
    5050lemma symbol_of_function_block_ok :
     
    6161qed.
    6262
     63(*
    6364definition funct_of_block : ∀F,ge.
    6465  block → option  (Σi.is_function F ge i) ≝
     
    193194>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
    194195qed.
    195 
     196*)
    196197
    197198include alias "common/PositiveMap.ma".
     
    234235qed.
    235236
    236 
    237 
     237lemma globalenv_no_zero :
     238 ∀F,V,i,p.
     239  find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
     240qed.
     241
Note: See TracChangeset for help on using the changeset viewer.