Changeset 1214 for src/common


Ignore:
Timestamp:
Sep 15, 2011, 2:27:50 PM (8 years ago)
Author:
sacerdot
Message:

res_to_opt function added to common/Errors and used in joint/semantics to make
the code look nicer

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1125 r1214  
    238238#A #m #P #e elim e; /2/;
    239239qed.
     240
     241definition res_to_opt : ∀A:Type[0]. res A → option A ≝
     242 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracChangeset for help on using the changeset viewer.