Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/backEndOps.mli

    r2773 r2933  
    302302  BitVector.bit) Types.prod
    303303
     304val op_of_add_or_sub : ByteValues.add_or_sub -> op2
     305
    304306val be_add_sub_byte :
    305   Bool.bool -> ByteValues.bebit -> ByteValues.beval -> BitVector.byte ->
    306   (ByteValues.beval, ByteValues.bebit) Types.prod Errors.res
     307  ByteValues.add_or_sub -> ByteValues.bebit -> ByteValues.beval ->
     308  BitVector.byte -> (ByteValues.beval, ByteValues.bebit) Types.prod
     309  Errors.res
    307310
    308311val byte_at : Nat.nat -> BitVector.bitVector -> Nat.nat -> BitVector.byte
Note: See TracChangeset for help on using the changeset viewer.