Changeset 2208 for src/LTL


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (7 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL_paolo.ma

    r2174 r2208  
    1818unification hint 0 ≔
    1919(*---------------*) ⊢
    20 snd_arg ltl_params ≡ ltl_argument.
     20snd_arg ltl_params ≡ hdw_argument.
    2121unification hint 0 ≔
    2222(*---------------*) ⊢
     
    2727
    2828definition ltl_program ≝ joint_program ltl_params.
     29
     30coercion byte_to_ltl_argument : ∀b: Byte.snd_arg ltl_params ≝
     31  hdw_argument_from_byte on _b : Byte to snd_arg ltl_params.
     32coercion reg_to_ltl_argument : ∀r: Register.snd_arg ltl_params ≝
     33  hdw_argument_from_reg on _r : Register to snd_arg ltl_params.
Note: See TracChangeset for help on using the changeset viewer.