Changeset 2608 for src/common/extraGlobalenvs.ma
 Timestamp:
 Feb 6, 2013, 1:01:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2590 r2608 219 219 ** #x1 #x2 #x3 #tl whd in match add_globals; 220 220 normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta 221 cases(alloc m ? ? x2) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;221 cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol; 222 222 normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %] 223 223 #f1 #H3 <(drop_fn_lfn … f1 H3) assumption … … 227 227 lemma globalenv_no_minus_one : 228 228 ∀F,V,i,p. 229 find_funct_ptr … (globalenv F V i p) (mk_block Code(1)) = None ?.229 find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (1)) = None ?. 230 230 #F #V #i #p 231 231 whd in match find_funct_ptr; normalize nodelta … … 237 237 lemma globalenv_no_zero : 238 238 ∀F,V,i,p. 239 find_funct_ptr … (globalenv F V i p) (mk_block CodeOZ) = None ?. //240 qed. 241 239 find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. // 240 qed. 241
Note: See TracChangeset
for help on using the changeset viewer.