Changeset 714 for src/ASM/ASM.ma


Ignore:
Timestamp:
Mar 29, 2011, 12:24:45 PM (10 years ago)
Author:
mulligan
Message:

Work on translation from LTL to LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r698 r714  
    9696  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    9797     is_a he A ∨ is_in ? tl A ].
    98 
    99 definition bool_to_Prop ≝
    100  λb. match b with [ true ⇒ True | false ⇒ False ].
    10198
    10299record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.