Changeset 3376
- Timestamp:
- Jul 1, 2013, 5:55:43 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Imp.ma
r3375 r3376 66 66 67 67 definition state: storeT → Type[0] ≝ λS. 68 cmd × continuation × ((list ( ident × (option label) × continuation)) × S).68 cmd × continuation × ((list (nat × ident × ((option label) × continuation))) × S). 69 69 70 70 definition fetchT ≝ fname → cmd. … … 116 116 step … 117 117 〈Ccall x f e l, k, K, s〉 118 〈c, [], 〈 x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉118 〈c, [], 〈get ? s (None …),x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉 119 119 (Some … f) 120 | step_return: ∀e,k1, x,l,k2,K,s.120 | step_return: ∀e,k1,v,x,l,k2,K,s. 121 121 step … 122 〈Cret e, k1, 〈 x,l,k2〉::K, s〉123 〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)〉122 〈Cret e, k1, 〈v,x,l,k2〉::K, s〉 123 〈Cskip, k2, K, set ? (set ? s (Some … x) (eval_expr ? s e)) (None …) v〉 124 124 l. 125 125
Note: See TracChangeset
for help on using the changeset viewer.