Nuprl Definition : fn_array
fn_array{i:l}(Val;n) == mk_array(ℕn ⟶ Val;λi,f. (f i);λi,v,f,k. if (k =z i) then v else f k fi ;λv,i. v)
Definitions occuring in Statement :
mk_array: mk_array(Arr;idx;upd;newarray),
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
mk_array: mk_array(Arr;idx;upd;newarray),
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
fn_array
Latex:
fn\_array\{i:l\}(Val;n) == mk\_array(\mBbbN{}n {}\mrightarrow{} Val;\mlambda{}i,f. (f i);\mlambda{}i,v,f,k. if (k =\msubz{} i) then v else f k fi ;\mlambda{}v\000C,i. v)
Date html generated:
2016_05_15-PM-02_17_40
Last ObjectModification:
2015_09_23-AM-07_38_30
Theory : monads
Home
Index