Changeset 889 for src/ASM/Vector.ma
- Timestamp:
- Jun 6, 2011, 11:07:24 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Vector.ma
r873 r889 338 338 | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉ 339 339 ]. 340 >plus_n_Sm_fast @refl qed.340 < plus_n_Sm_fast @refl qed. 341 341 342 342 let 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.