Nuprl Definition : ml_insert_int

ml_insert_int(x;l) ==
  fix((λinsert_int,x,l. if null(l)
                       then [x]
                       else let a.as = l 
                            in if x <z a + 1 then [x / l] else [a / insert_int(x)(as)] fi 
                       fi )) 
  x 
  l


Definitions occuring in Statement :  spreadcons: spreadcons,  ml_apply: f(x),  null: null(as),  cons: [a / b],  nil: [],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  add: n + m,  natural_number: $n
Definitions occuring in definition :  apply: f a,  fix: fix(F),  lambda: λx.A[x],  null: null(as),  nil: [],  spreadcons: spreadcons,  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  add: n + m,  natural_number: $n,  cons: [a / b],  ml_apply: f(x)
FDL editor aliases :  ml_insert_int
Latex:
ml\_insert\_int(x;l)  ==
    fix((\mlambda{}insert$_{int}$,x,l.  if  null(l)
                                            then  [x]
                                            else  let  a.as  =  l 
                                                      in  if  x  <z  a  +  1  then  [x  /  l]  else  [a  /  insert$_{int}\mbackslash{}ff2\000C4(x)(as)]  fi 
                                            fi  )) 
    x 
    l


Date html generated: 2017_09_29-PM-05_51_19
Last ObjectModification: 2017_05_11-PM-05_13_09

Theory : ML


Home Index