Changeset 749


Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Make definition more explicit to avoid jmeq.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r744 r749  
    409409(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
    410410definition 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 ].
    412412
    413413definition shift_right_1 ≝
Note: See TracChangeset for help on using the changeset viewer.