source: src/common/StatusSimulation.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @2870   8 years sacerdot Proof fixed.
(edit) @2869   8 years tranquil some reorganization of definitions, and a new taaf_append_taaf
(edit) @2799   8 years tranquil * added taaf_to_taa, conversion from trace_any_any_free to …
(edit) @2756   8 years sacerdot WARNING: this commit breaks things, sorry, Paolo is going to fix …
(edit) @2755   8 years tranquil * changed primitives of abstract status (with stuf that is probably …
(edit) @2553   8 years tranquil as_classify changed to a partial function added a status for tailcalls
(edit) @2540   8 years tranquil cl_jump case now provides a proof of costedness of the following state
(edit) @2539   8 years tranquil added cl_jump case to trace_any_any_free
(edit) @2530   8 years tranquil temporary switch to cl_jump treated as cl_other fixed script for new …
(edit) @2477   8 years tranquil status_simulation reformulated definition of joint_classify split up …
(edit) @2463   8 years tranquil swapped back call_rel and ret_rel…
(edit) @2457   8 years tranquil rewritten function handling in joint swapped call_rel with ret_rel in …
(edit) @2436   8 years tranquil small changes
(edit) @2421   8 years tranquil added simulation of flat prefix, and comments to explain the code
(add) @2413   8 years tranquil * tal_rel corrected to include cases where tal_base_call \approx …
Note: See TracRevisionLog for help on using the revision log.