Nuprl Definition : insert-int
insert-int(x;l) == rec-case(l) of [] => [x] | a::as => v.if (a) < (x) then eval y = v in [a / y] else [x; [a / as]]
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d
Definitions occuring in definition :
list_ind: list_ind,
nil: [],
less: if (a) < (b) then c else d,
callbyvalue: callbyvalue,
cons: [a / b]
FDL editor aliases :
insert-int
Latex:
insert-int(x;l) ==
rec-case(l) of
[] => [x]
a::as =>
v.if (a) < (x) then eval y = v in [a / y] else [x; [a / as]]
Date html generated:
2017_09_29-PM-05_48_21
Last ObjectModification:
2017_05_03-PM-00_10_41
Theory : list_0
Home
Index