Changeset 1976 for src/utilities/option.ma

Timestamp:

May 21, 2012, 7:04:21 PM (9 years ago)

Author:

tranquil

Message:

• monads: just changed some defs, which had to be propagated in some files
• ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
• added a library for permutations of lists (useful with fold AC ops on lists)
• first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)

File:

• src/utilities/option.ma (modified) (1 diff)

src/utilities/option.ma

@@ -62 +62 @@
 interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
 
-definition OptPred ≝ λPdef : Prop.mk_MonadPred Option
-  (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
+definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option
+  (mk_MonadPred ?
+    (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
+    ???)
   (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ])
-  ????.
-[ @prf
+  ?.
+[4: @prf
 |*:
-#X[2:#Y]#P1[1,3:#P2[2:#H]]
+#X[2:#Y]#P1[1,2:#P2[2:#H]]
 [1,2,4: * [5: *]] normalize /2/
 qed.