source: src/utilities/option.ma @ 1183

Last change on this file since 1183 was 761, checked in by campbell, 10 years ago

Enforce the use of declared identifiers/registers in Cminor/RTLabs.
File size: 179 bytes
RevLine 
[761]1include "basics/types.ma".
2
3definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
4λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
Note: See TracBrowser for help on using the repository browser.