Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/option.ma

    r1949 r1976  
    6262interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
    6363
    64 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option
    65   (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
     64definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option
     65  (mk_MonadPred ?
     66    (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
     67    ???)
    6668  (λ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 [ @prf
     69  ?.
     70[4: @prf
    6971|*:
    70 #X[2:#Y]#P1[1,3:#P2[2:#H]]
     72#X[2:#Y]#P1[1,2:#P2[2:#H]]
    7173[1,2,4: * [5: *]] normalize /2/
    7274qed.
Note: See TracChangeset for help on using the changeset viewer.