Changeset 889


Ignore:
Timestamp:
Jun 6, 2011, 11:07:24 PM (8 years ago)
Author:
sacerdot
Message:

Minor changes because of the new, weaker (but much faster) delift.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r885 r889  
    762762     @eq_instruction_refl
    763763   | cases arg -i arg;
     764(* 
     76516,17,18,19,20,28,19
     766*)
    764767     [1,2,3: #arg1 #arg2
    765768       @(list_addressing_mode_tags_elim_prop … arg1) whd try %
     
    833836       >half_add_SO
    834837       >lookup_insert_hit
    835        >lookup_insert_miss try @not_eqvb_SS
     838       >lookup_insert_miss //
    836839       >lookup_insert_hit
    837840       normalize
  • src/ASM/Vector.ma

    r873 r889  
    338338    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
    339339    ].
    340 > plus_n_Sm_fast @refl qed.
     340< plus_n_Sm_fast @refl qed.
    341341
    342342let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
  • src/common/Integers.ma

    r747 r889  
    434434theorem eq_sym:
    435435  ∀x,y. eq x y = eq y x.
    436 #x #y @eq_bv_elim @eq_bv_elim /2/
     436#x #y change with (eq_bv ??? = eq_bv ???)
     437 @eq_bv_elim @eq_bv_elim /2/
    437438[ #NE #E @False_ind >E in NE * /2/
    438439| #E #NE @False_ind >E in NE * /2/
     
    440441
    441442theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y).
    442 #x #y @eq_bv_elim #H @H qed.
     443#x #y change with (if eq_bv ? x y then ? else ?) @eq_bv_elim #H @H qed.
    443444
    444445theorem eq_true: ∀x. eq x x = true.
Note: See TracChangeset for help on using the changeset viewer.