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 let y = insert_int(x)(as) in [a / y] 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,
let: let,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
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,
let: let,
ml_apply: f(x),
cons: [a / b]
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 let y = insert$_{int}\mbackslash{}\000Cff24(x)(as) in [a / y] fi
fi ))(x)(l)
Date html generated:
2017_09_29-PM-05_51_04
Last ObjectModification:
2017_05_10-PM-06_58_17
Theory : ML
Home
Index