added datatype order;
authorwenzelm
Mon Jan 13 18:20:35 1997 +0100 (1997-01-13)
changeset 2506965127966331
parent 2505 50abca9d4043
child 2507 d290b91e76b8
added datatype order;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Jan 13 13:20:32 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Jan 13 18:20:35 1997 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  Basic library: functions, options, pairs, booleans, lists, integers,
     1.6  strings, lists as sets, association lists, generic tables, balanced trees,
     1.7 -input / output, timing, filenames, misc functions.
     1.8 +orders, input / output, timing, filenames, misc functions.
     1.9  *)
    1.10  
    1.11  infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    1.12 @@ -689,6 +689,22 @@
    1.13  
    1.14  
    1.15  
    1.16 +(** orders **)
    1.17 +
    1.18 +datatype order = LESS | EQUAL | GREATER;
    1.19 +
    1.20 +fun intord (i, j: int) =
    1.21 +  if i < j then LESS
    1.22 +  else if i = j then EQUAL
    1.23 +  else GREATER;
    1.24 +
    1.25 +fun stringord (a, b: string) =
    1.26 +  if a < b then LESS
    1.27 +  else if a = b then EQUAL
    1.28 +  else GREATER;
    1.29 +
    1.30 +
    1.31 +
    1.32  (** input / output **)
    1.33  
    1.34  val cd = OS.FileSys.chDir;