Changeset 1311 for Deliverables/D3.3/id-lookup-branch/ASM
- Timestamp:
- Oct 6, 2011, 6:45:54 PM (9 years ago)
- Location:
- Deliverables/D3.3/id-lookup-branch
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch
- Property svn:mergeinfo changed
/src merged: 1198,1206-1233,1236-1260,1262-1264,1266,1268-1271,1274-1276,1278-1290,1292
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ASM
- Property svn:mergeinfo changed
/src/ASM merged: 1207,1279
- Property svn:mergeinfo changed
-
Deliverables/D3.3/id-lookup-branch/ASM/Arithmetic.ma
r961 r1311 319 319 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". 320 320 321 definition max_u ≝ λn,a,b. if lt_u n a b then b else a. 322 definition min_u ≝ λn,a,b. if lt_u n a b then a else b. 323 definition max_s ≝ λn,a,b. if lt_s n a b then b else a. 324 definition min_s ≝ λn,a,b. if lt_s n a b then a else b. 325 321 326 definition bitvector_of_bool: 322 327 ∀n: nat. ∀b: bool. BitVector (S n) ≝ -
Deliverables/D3.3/id-lookup-branch/ASM/Util.ma
r1197 r1311 40 40 definition gtb ≝ 41 41 λm, n: nat. 42 l eb n m.42 ltb n m. 43 43 44 44 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
Note: See TracChangeset
for help on using the changeset viewer.