% $Id: WadlerProps.lsl,v 1.4 2000/01/17 21:33:40 connolly Exp $
%

WadlerProps: trait
    includes
        XPathWadler

    introduces
        M': Pattern, Node ® Bool
% Wadler writes Pattern x Node -> Bool, but then uses
% it as a higher-order function. odd.

    asserts forall p, p1: Pattern,
                   x, x1, x2: Node,
                   s: String

        M'(p, x) = $ x1 (x1 Î (parent*)[x]
                           Ù x Î S(p)[x1]);

    implies forall p, p1: Pattern, x: Node, s: String

%@@ p not containing id(p), ancestor(p), ancestor-or-self(p), ..
%M(p, x) = M'(p, x);

        p = !p1 Ú p = id(s) Þ
            S(p)[x] = S(p)[root(x)];

% p @@ not containing /p, id(s), ancestor(p), anc-or-self(p), ..
%S(p)[x] \subseteq (subnodes\superstar)[x];

%@@ save this for later...
% S(p!id(dot))[x] = S(id(p))[x];

[Index]

[source]

HTML generated using lsl2html.