TFL/mask.sml
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2112 3902e9af752f
child 3302 404fe31fd8d2
permissions -rw-r--r--
moved settings comment to build;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
(*---------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
 * This structure is intended to shield TFL from any constructors already 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
 * declared in the environment. In the Isabelle port, for example, there
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
 * was already a datatype with "|->" being a constructor. In TFL we were
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
 * trying to define a function "|->", but it failed in PolyML (which conforms
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
 * better to the Standard) while the definition was accepted in NJ/SML
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
 * (which doesn't always conform so well to the standard).
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
 *---------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
structure Mask : Mask_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
struct
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
 datatype 'a binding = |-> of ('a * 'a)   (* infix 7 |->; *)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
 datatype mask = ERR 
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
end;