Changeset 889 for src/ASM/Vector.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 ≝
Note: See TracChangeset for help on using the changeset viewer.