Changeset 1233 for src/common


Ignore:
Timestamp:
Sep 21, 2011, 11:57:20 AM (8 years ago)
Author:
sacerdot
Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r1231 r1233  
    44include "common/Events.ma".
    55
    6 record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    7 { global : Type[0]
     6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
     7{ global : Type[1]
    88; state  : global → Type[0]
    99; is_final : ∀g. state g → option int
     
    8080*)
    8181
    82 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     82record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
    8383{ program : Type[0]
    8484; es1 :> trans_system outty inty
Note: See TracChangeset for help on using the changeset viewer.