Changeset 1782
- Timestamp:
- Feb 27, 2012, 5:55:27 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1765 r1782 1534 1534 #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -NOT_UNDEFINED -NO_TERMINATION destruct 1535 1535 inversion S 1536 [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H133 #H134 #H135 #H136 #H137 #H138 #H139destruct ]1536 [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ] 1537 1537 (* state_bound_on_steps_to_cost needs to know about the current stack frame, 1538 1538 so we can use it as a witness that at least one frame exists *)
Note: See TracChangeset
for help on using the changeset viewer.