% @(#)$Id: WidenNarrow.lsl,v 1.3 1997/02/13 00:21:25 leavens Exp $
% Maps between untyped and typed values.
% This could be used to describe any partially inverse pair of mappings.
WidenNarrow(Typed, Untyped): trait
  introduces 
    widen: Typed -> Untyped
    narrow: Untyped -> Typed
  asserts
    \forall t: Typed
       narrow(widen(t)) == t;
  implies
    \forall u: Untyped
       narrow(widen(narrow(u))) == narrow(u);

[Index]

HTML generated using lcpp2html.