Changeset 1214 for src/common

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:

• src/common/Errors.ma (modified) (1 diff)

src/common/Errors.ma

@@ -238 +238 @@
 #A #m #P #e elim e; /2/;
 qed.
+
+definition res_to_opt : ∀A:Type[0]. res A → option A ≝
+ λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].