Ignore:
Timestamp:
Apr 19, 2011, 12:22:32 PM (10 years ago)
Author:
campbell
Message:

Enforce the use of declared identifiers/registers in Cminor/RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Coqlib.ma

    r747 r761  
    599599(* * Mapping a function over an option type. *)
    600600
    601 definition option_map ≝ λA,B.λf:A→B.λv:option A.
    602   match v with [ Some v' ⇒ Some ? (f v') | None ⇒ None ? ].
     601include "utilities/option.ma".
    603602
    604603(*
Note: See TracChangeset for help on using the changeset viewer.