/usr/share/hol88-2.02.19940316/Library/trs/sets.ml is in hol88-library-source 2.02.19940316-19.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | % sets.ml (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%
% Function to determine whether a list contains any repetitions %
letrec no_rep l =
% : (* list -> bool) %
if (null l)
then true
else if (mem (hd l) (tl l))
then false
else no_rep (tl l);;
% Function to remove any repetitions in a list %
letrec remove_rep l =
% : (* list -> * list) %
if (null l)
then []
else if (mem (hd l) (tl l))
then (remove_rep (tl l))
else (hd l).(remove_rep (tl l));;
% Function to determine if one list (containing no repetitions) is a %
% subset of another list (containing no repetitions). %
% The function tests if subl is a subset of l by subtracting (setwise) l %
% from subl. If this gives a null list, then subl is a subset of l. %
let is_subset l subl = null (subtract subl l);;
% : (* list -> * list -> bool) %
%----------------------------------------------------------------------------%
|