Changeset 878 for src/RTLabs
- Timestamp:
- Jun 3, 2011, 5:35:27 PM (10 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/import.ma
r816 r878 23 23 ; pf_exit : nat 24 24 }. 25 (* XXX projection generation with nat broken *)26 definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].27 definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].28 definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].29 definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].30 25 31 26 definition make_register : -
src/RTLabs/syntax.ma
r816 r878 70 70 ; f_exit : label 71 71 }. 72 (* XXX: matita interpretations bug workaround *)73 definition f_stacksize : internal_function → nat ≝74 λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _ _ ⇒ s ].75 72 76 73 (* Note that the global variables will be initialised by the code in main
Note: See TracChangeset
for help on using the changeset viewer.