Changeset 1516 for src/common/Pointers.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Pointers.ma
r1215 r1516 34 34 P (eq_block b1 b2). 35 35 #P * #r1 #i1 * #r2 #i2 #H1 #H2 36 whd in ⊢ (?%) @eq_region_elim #H337 [ whd in ⊢ (?%) @eqZb_elim [ /2/  * #NE @H2 % #E @NE destruct % ]36 whd in ⊢ (?%); @eq_region_elim #H3 37 [ whd in ⊢ (?%); @eqZb_elim [ /2/  * #NE @H2 % #E @NE destruct % ] 38 38  @H2 % #E destruct elim H3 /2/ 39 39 ] qed. 40 40 41 41 lemma eq_block_b_b : ∀b. eq_block b b = true. 42 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl42 * * #z whd in ⊢ (??%?); >eqZb_z_z @refl 43 43 qed. 44 44 … … 71 71 72 72 lemma reflexive_eq_offset: ∀x. eq_offset x x = true. 73 whd in match eq_offset /2/73 whd in match eq_offset; /2/ 74 74 qed. 75 75 … … 109 109 110 110 lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. 111 #p whd in ⊢ (??%?) >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //111 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // 112 112 qed.
Note: See TracChangeset
for help on using the changeset viewer.