Nuprl Definition : ml_merge_int
ml_merge_int(as;bs) ==
λas,bs. ml-reduce(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 ));as;bs)(as)(bs)
Definitions occuring in Statement :
ml-reduce: ml-reduce(f;b;l),
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,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
ml-reduce: ml-reduce(f;b;l),
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_merge_int
Latex:
ml\_merge\_int(as;bs) ==
\mlambda{}as,bs. ml-reduce(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}$(x)(as)]
fi
fi ));as;bs)(as)(bs)
Date html generated:
2017_09_29-PM-05_51_22
Last ObjectModification:
2017_05_11-PM-03_36_38
Theory : ML
Home
Index