Nuprl Definition : eval-mklist
eval-mklist(n;f;offset) ==
  if n=0
  then []
  else eval v = f offset in
       eval offset' = offset + 1 in
       eval n' = n - 1 in
       eval L = eval-mklist(n';f;offset') in
         [v / L]
Definitions occuring in Statement : 
cons: [a / b]
, 
nil: []
, 
callbyvalue: callbyvalue, 
int_eq: if a=b then c else d
, 
apply: f a
, 
subtract: n - m
, 
add: n + m
, 
natural_number: $n
Definitions occuring in definition : 
int_eq: if a=b then c else d
, 
nil: []
, 
apply: f a
, 
add: n + m
, 
subtract: n - m
, 
natural_number: $n
, 
callbyvalue: callbyvalue, 
cons: [a / b]
FDL editor aliases : 
eval-mklist
Latex:
eval-mklist(n;f;offset)  ==
    if  n=0
    then  []
    else  eval  v  =  f  offset  in
              eval  offset'  =  offset  +  1  in
              eval  n'  =  n  -  1  in
              eval  L  =  eval-mklist(n';f;offset')  in
                  [v  /  L]
Date html generated:
2019_06_20-PM-01_31_10
Last ObjectModification:
2019_01_21-AM-10_53_14
Theory : list_1
Home
Index