Changeset 2796 for src/common


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/ErrorMessages.ma

    r2795 r2796  
    7070 | BadCostLabelling : ErrorMessage
    7171 | RepeatedCostLabel : ErrorMessage
    72  | NotTerminated : ErrorMessage.
     72 | NotTerminated : ErrorMessage
     73 | RepeatedCostLabel : ErrorMessage
     74 | FramesEmptyOnPop : ErrorMessage
     75 | BlockInFramesCorrupted : ErrorMessage
     76 | FrameErrorOnPush : ErrorMessage
     77 | FrameErrorOnPop : ErrorMessage.
Note: See TracChangeset for help on using the changeset viewer.