Nuprl Definition : simple-swap
simple-swap(AModel;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(λin@j.(A-bind(AModel) (A-assign(AModel) i in@j) (λx.(A-assign(AModel) j in@i))))))
Definitions occuring in Statement :
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
A-assign: A-assign(AModel),
A-bind: A-bind(AModel),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
A-bind: A-bind(AModel),
lambda: λx.A[x],
apply: f a,
A-assign: A-assign(AModel)
FDL editor aliases :
simple-swap
Latex:
simple-swap(AModel;i;j) ==
A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}in@i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) j))
(\mlambda{}in@j.(A-bind(AModel) (A-assign(AModel) i in@j) (\mlambda{}x.(A-assign(AModel) j in@i))))))
Date html generated:
2016_05_15-PM-02_20_09
Last ObjectModification:
2015_09_23-AM-07_38_45
Theory : monads
Home
Index