Changeset 889 for src/ASM/Vector.ma

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:

• src/ASM/Vector.ma (modified) (1 diff)

src/ASM/Vector.ma

@@ -338 +338 @@
     | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
     ].
-> plus_n_Sm_fast @refl qed.
+< plus_n_Sm_fast @refl qed.
 
 let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝