Ignore:
Timestamp:
Jun 17, 2011, 1:30:01 PM (9 years ago)
Author:
sacerdot
Message:

Do no longer use the daemon automatically :-)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r985 r990  
    133133 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    134134  [ #w #_ %1 %[@w] %
    135   | #n #l #r #abs @⊥ //
     135  | #n #l #r #abs @⊥ destruct(abs)
    136136  | #n #EQ %2 >EQ %]
    137137qed.
     
    140140 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    141141 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    142   [ #m #abs @⊥ //
     142  [ #m #abs @⊥ destruct(abs)
    143143  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    144144  | #m #EQ %2 // ]
Note: See TracChangeset for help on using the changeset viewer.