Nuprl Definition : A-loop

A-loop(AType;lo;hi;body) ==
  fix((λA-loop,hi. if hi ≤z lo
                  then A-null(AType)
                  else A-bind(array-model(AType)) (A-loop (hi - 1)) (λx.(body (hi - 1)))
                  fi )) 
  hi


Definitions occuring in Statement :  A-null: A-null(AType),  A-bind: A-bind(AModel),  array-model: array-model(AType),  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  ifthenelse: if b then t else f fi ,  le_int: i ≤z j,  A-null: A-null(AType),  A-bind: A-bind(AModel),  array-model: array-model(AType),  lambda: λx.A[x],  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  A-loop
Latex:
A-loop(AType;lo;hi;body)  ==
    fix((\mlambda{}A-loop,hi.  if  hi  \mleq{}z  lo
                                    then  A-null(AType)
                                    else  A-bind(array-model(AType))  (A-loop  (hi  -  1))  (\mlambda{}x.(body  (hi  -  1)))
                                    fi  )) 
    hi


Date html generated: 2016_05_15-PM-02_19_25
Last ObjectModification: 2015_09_23-AM-07_38_40

Theory : monads


Home Index