Ignore:
Timestamp:
Mar 1, 2013, 11:06:29 AM (8 years ago)
Author:
tranquil
Message:
  • changed primitives of abstract status (with stuf that is probably already there in all of its implementations): this temporarily breaks current as creations
  • generalised stacksize file and consequently moved it to common
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2553 r2755  
    707707
    708708(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
    709 
    710 inductive intensional_event : Type[0] ≝
    711 | IEVcost : costlabel → intensional_event
    712 | IEVcall : ident → intensional_event
    713 | IEVtailcall : ident → ident → intensional_event
    714 | IEVret : ident → intensional_event.
    715 
    716709let rec ft_observables_aux acc S st st' stack
    717710  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
Note: See TracChangeset for help on using the changeset viewer.