Nuprl Definition : insert-no-combine
insert-no-combine(cmp;x;l) == rec-case(l) of [] => [x] | a::as => v.if 0 ≤z cmp x a then [x; [a / as]] else [a / v] fi
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
apply: f a,
natural_number: $n
Definitions occuring in definition :
list_ind: list_ind,
nil: [],
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
natural_number: $n,
apply: f a,
cons: [a / b]
FDL editor aliases :
insert-no-combine
Latex:
insert-no-combine(cmp;x;l) ==
rec-case(l) of
[] => [x]
a::as =>
v.if 0 \mleq{}z cmp x a then [x; [a / as]] else [a / v] fi
Date html generated:
2016_05_14-PM-02_42_52
Last ObjectModification:
2015_09_22-PM-05_57_26
Theory : list_1
Home
Index