 Timestamp:
 Apr 12, 2011, 12:32:33 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Vector.ma
r744 r749 409 409 (* XXX this is horrible  but useful to ensure that we can normalise in the proof assistant. *) 410 410 definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝ 411 λA,n,m. match commutative_plus_faster n m with [ refl ⇒ λi.i ].411 λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ]. 412 412 413 413 definition shift_right_1 ≝
Note: See TracChangeset
for help on using the changeset viewer.