Changeset 1119


Ignore:
Timestamp:
Aug 26, 2011, 7:38:59 PM (8 years ago)
Author:
sacerdot
Message:

Type for evaluation of opaccs fixed (maybe wrongly: should it return
Byte \times Byte or option (Byte \times Byte)?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1094 r1119  
    32423242record Eval: Type[0] ≝
    32433243{
    3244   opaccs: OpAccs → Byte → Byte → option Byte;
     3244  opaccs: OpAccs → Byte → Byte → Byte × Byte;
    32453245  op1: Op1 → Byte → Byte;
    32463246  op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
    32473247}.
    32483248
    3249 axiom opaccs_implementation: OpAccs → Byte → Byte → option Byte.
     3249axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    32503250axiom op1_implementation: Op1 → Byte → Byte.
    32513251axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
Note: See TracChangeset for help on using the changeset viewer.