Nuprl Definition : array-model
array-model(AType) ==
<M-return(array-monad(AType))
, M-bind(array-monad(AType))
, λv,m. (fst((m (newarray(AType) v))))
, λi,v,A. <⋅, upd(AType) i v A>
, M-return(array-monad'(AType))
, M-bind(array-monad'(AType))
, λi,A. (idx(AType) i A)
, λm,A. <m A, A>
, M-map(array-monad(AType))
, M-map(array-monad'(AType))
, λm,A. (fst((m A)))>
Definitions occuring in Statement :
array-monad': array-monad'(AType),
array-monad: array-monad(AType),
newarray: newarray(AType),
upd: upd(AType),
idx: idx(AType),
M-bind: M-bind(Mnd),
M-return: M-return(Mnd),
M-map: M-map(mnd),
it: ⋅,
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
newarray: newarray(AType),
it: ⋅,
upd: upd(AType),
M-return: M-return(Mnd),
M-bind: M-bind(Mnd),
idx: idx(AType),
array-monad: array-monad(AType),
pair: <a, b>,
M-map: M-map(mnd),
array-monad': array-monad'(AType),
lambda: λx.A[x],
pi1: fst(t),
apply: f a
FDL editor aliases :
array-model
Latex:
array-model(AType) ==
<M-return(array-monad(AType))
, M-bind(array-monad(AType))
, \mlambda{}v,m. (fst((m (newarray(AType) v))))
, \mlambda{}i,v,A. <\mcdot{}, upd(AType) i v A>
, M-return(array-monad'(AType))
, M-bind(array-monad'(AType))
, \mlambda{}i,A. (idx(AType) i A)
, \mlambda{}m,A. <m A, A>
, M-map(array-monad(AType))
, M-map(array-monad'(AType))
, \mlambda{}m,A. (fst((m A)))>
Date html generated:
2016_05_15-PM-02_18_09
Last ObjectModification:
2015_09_23-AM-07_38_31
Theory : monads
Home
Index