Changeset 2796 for src/ERTLptr


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (8 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
Location:
src/ERTLptr
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr_semantics.ma

    r2783 r2796  
    5656  (* read_result        ≝ *) (λ_.λ_.λ_.
    5757     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    58   (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
     58  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertlptr_seq F gl ge stm id)
    5959  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
    6060 
Note: See TracChangeset for help on using the changeset viewer.