Ignore:
Timestamp:
Feb 22, 2013, 7:11:30 PM (7 years ago)
Author:
tranquil
Message:

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/state.ma

    r1976 r2708  
    2424definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
    2525definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
     26definition state_update : ∀S.(S → S) → state_monad S unit ≝ λS,f,s.〈f s, it〉.
    2627
    2728definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
Note: See TracChangeset for help on using the changeset viewer.