Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r1215 r1516  
    3434  P (eq_block b1 b2).
    3535#P * #r1 #i1 * #r2 #i2 #H1 #H2
    36 whd in ⊢ (?%) @eq_region_elim #H3
    37 [ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
     36whd in ⊢ (?%); @eq_region_elim #H3
     37[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
    3838| @H2 % #E destruct elim H3 /2/
    3939] qed.
    4040
    4141lemma eq_block_b_b : ∀b. eq_block b b = true.
    42 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl
     42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
    4343qed.
    4444
     
    7171
    7272lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
    73  whd in match eq_offset /2/
     73 whd in match eq_offset; /2/
    7474qed.
    7575
     
    109109
    110110lemma 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 //
    112112qed.
Note: See TracChangeset for help on using the changeset viewer.