Ignore:
Timestamp:
Mar 26, 2013, 3:52:39 PM (7 years ago)
Author:
tranquil
Message:

resolved circular dependency for ERTLptr's semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2952 r2954  
    405405λp,prog,stacksizes.
    406406let genv ≝ globalenv … (λx.x) prog in
    407 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog).
     407let pc_from_lbl ≝ λbl.λfn : joint_closed_internal_function p ?.λlbl.
     408  ! pt ← point_of_label … (joint_if_code … fn) lbl ;
     409  return mk_program_counter bl (offset_of_point … p pt) in
     410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl.
    408411#s #H
    409412elim (find_symbol_exists ?? (λx.x) … prog s ?)
    410413[ #bl #EQ >EQ % #ABS destruct ]
    411414@Exists_append_r
    412 @(Exists_mp … H) //
     415@(Exists_mp … H) @sym_eq
    413416qed.
    414417
Note: See TracChangeset for help on using the changeset viewer.