Nuprl Definition : shadow-vec
shadow-vec(i;as;bs) ==
  eval bs' = evalall(as[i] * bs) in
  eval as' = evalall(-bs[i] * as) in
  eval L = evalall(bs' + as') in
    evalall(L\i)
Definitions occuring in Statement : 
int-vec-add: as + bs
, 
int-vec-mul: a * as
, 
list-delete: as\i
, 
select: L[n]
, 
evalall: evalall(t)
, 
callbyvalue: callbyvalue, 
minus: -n
Definitions occuring in definition : 
int-vec-mul: a * as
, 
minus: -n
, 
select: L[n]
, 
callbyvalue: callbyvalue, 
int-vec-add: as + bs
, 
evalall: evalall(t)
, 
list-delete: as\i
FDL editor aliases : 
shadow-vec
Latex:
shadow-vec(i;as;bs)  ==
    eval  bs'  =  evalall(as[i]  *  bs)  in
    eval  as'  =  evalall(-bs[i]  *  as)  in
    eval  L  =  evalall(bs'  +  as')  in
        evalall(L\mbackslash{}i)
Date html generated:
2016_05_14-AM-06_57_23
Last ObjectModification:
2015_09_22-PM-05_51_19
Theory : omega
Home
Index