Changeset 1976 for src/utilities/option.ma
- Timestamp:
- May 21, 2012, 7:04:21 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/option.ma
r1949 r1976 62 62 interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f). 63 63 64 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option 65 (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef) 64 definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option 65 (mk_MonadPred ? 66 (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef) 67 ???) 66 68 (λ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 ]) 67 ? ???.68 [ @prf69 ?. 70 [4: @prf 69 71 |*: 70 #X[2:#Y]#P1[1, 3:#P2[2:#H]]72 #X[2:#Y]#P1[1,2:#P2[2:#H]] 71 73 [1,2,4: * [5: *]] normalize /2/ 72 74 qed.
Note: See TracChangeset
for help on using the changeset viewer.