Changeset 1339 for src/common
- Timestamp:
- Oct 10, 2011, 4:10:32 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Values.ma
r1213 r1339 1186 1186 lemma zero_ext_lessdef: 1187 1187 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2). 1188 #n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //1188 #n #v1 #v2 #H inversion H // 1189 1189 qed. 1190 1190 1191 1191 lemma sign_ext_lessdef: 1192 1192 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2). 1193 #n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //1193 #n #v1 #v2 #H inversion H // 1194 1194 qed. 1195 1195 (*
Note: See TracChangeset
for help on using the changeset viewer.