Changeset 1524 for src/ASM


Ignore:
Timestamp:
Nov 21, 2011, 5:51:20 PM (8 years ago)
Author:
boender
Message:
  • adapted files to new Matita syntax
Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1521 r1524  
    373373
    374374lemma lookup_opt_lookup_miss:
    375   ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
     375  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.
    376376  lookup_opt A n b t = None A → ∀x.lookup A n b t x = x.
    377  #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
     377 #A #n #b #t generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
    378378 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct
    379379 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
  • src/ASM/Vector.ma

    r1516 r1524  
    180180  //
    181181  destruct
    182   //
    183182qed.
    184183
Note: See TracChangeset for help on using the changeset viewer.