Changeset 841 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 25, 2011, 2:33:44 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r840 r841 7 7 definition sigma: pseudo_assembly_program → option (Word → Word) ≝ 8 8 λinstr_list. 9 let result ≝ foldl ? (*(option (nat × (nat × (BitVectorTrie Word 16))))*)?9 let result ≝ foldl ?? 10 10 (λt. λi. 11 11 match t with … … 29 29 None ? 30 30 else 31 Some ? (λx.lookup ?? x sigma_map (zero …)) 32 ]. 31 Some ? (λx.lookup ?? x sigma_map (zero …)) ]. 33 32 34 33
Note: See TracChangeset
for help on using the changeset viewer.