Ignore:
Timestamp:
May 25, 2011, 2:33:44 PM (10 years ago)
Author:
sacerdot
Message:

Minor changes.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r840 r841  
    77definition sigma: pseudo_assembly_program → option (Word → Word) ≝
    88 λinstr_list.
    9   let result ≝ foldl ?(*(option (nat × (nat × (BitVectorTrie Word 16))))*) ?
     9  let result ≝ foldl ??
    1010    (λt. λi.
    1111       match t with
    … …  
    2929        None ?
    3030      else
    31         Some ? (λx.lookup ?? x sigma_map (zero …))
    32   ].
     31        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
    3332
    3433
Note: See TracChangeset for help on using the changeset viewer.