Changeset 1387


Ignore:
Timestamp:
Oct 17, 2011, 2:01:14 AM (8 years ago)
Author:
sacerdot
Message:

Further simplification *params1 no longer used.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1386 r1387  
    4848 }.
    4949
    50 record sem_params1: Type[1] ≝
    51  { spp1 :> params1
    52  ; ssucc_ : Type[0]
    53  ; more_sem_params1 :> more_sem_params (mk_params_ spp1 ssucc_)
    54  }.
    55 
    56 definition sem_params_of_sem_params1 ≝ λsp1: sem_params1. mk_sem_params … sp1.
    57 coercion sem_params_of_sem_params1 : ∀_x:sem_params1. sem_params
    58  ≝ sem_params_of_sem_params1 on _x: sem_params1 to sem_params.
    59 
    6050definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    6151
     
    8878coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
    8979 ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
    90 
    91 definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 sp2 (succ sp2) sp2.
    92 coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1
    93  ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1.
    9480
    9581definition address_of_label: sem_params → label → address.
Note: See TracChangeset for help on using the changeset viewer.