Changeset 1382 for src/LIN/semantics.ma


Ignore:
Timestamp:
Oct 14, 2011, 10:50:56 PM (8 years ago)
Author:
sacerdot
Message:
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/semantics.ma

    r1380 r1382  
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 (*CSC: XXXX*)
    5 axiom lin_succ_pc: unit → address → address.
     4definition lin_succ_pc: unit → address → res address :=
     5 λ_.λaddr. addr_add addr 1.
    66
    77(*CSC: XXXXXXXXXX *)
Note: See TracChangeset for help on using the changeset viewer.