Nuprl Definition : A-shift-upto
A-shift-upto(AType;j) ==
let AModel = array-model(AType) in
A-loop(AType;1;j;λi.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(λin@i.(A-assign(AModel) (i - 1) in@i))))
Definitions occuring in Statement :
A-loop: A-loop(AType;lo;hi;body),
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
A-assign: A-assign(AModel),
A-bind: A-bind(AModel),
array-model: array-model(AType),
let: let,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
let: let,
array-model: array-model(AType),
A-loop: A-loop(AType;lo;hi;body),
A-bind: A-bind(AModel),
A-coerce: A-coerce(AModel),
A-fetch': A-fetch'(AModel),
lambda: λx.A[x],
apply: f a,
A-assign: A-assign(AModel),
subtract: n - m,
natural_number: $n
FDL editor aliases :
A-shift-upto
Latex:
A-shift-upto(AType;j) ==
let AModel = array-model(AType) in
A-loop(AType;1;j;\mlambda{}i.(A-bind(AModel) (A-coerce(AModel) (A-fetch'(AModel) i))
(\mlambda{}in@i.(A-assign(AModel) (i - 1) in@i))))
Date html generated:
2016_05_15-PM-02_21_16
Last ObjectModification:
2015_09_23-AM-07_38_54
Theory : monads
Home
Index