% @(#)$Id: CoerceElements.lsl,v 1.2 1995/08/28 00:08:33 leavens Exp $
% Insert each element of Source[S] into a new Sink[T],
% using toT to coerce elements

CoerceElements(toT, SourceS, S, SinkT, T): trait
  assumes
    InsertGenerated(S, SourceS),
    InsertGenerated(T, SinkT),
    SimulationFun(toT, S, T)

  introduces
    coerce: SourceS -> SinkT

  asserts
   \forall source: SourceS, e: S
    coerce(empty) == empty;
    coerce(insert(e, source)) == insert(toT(e), coerce(source));

  implies
    converts coerce

[Index]

HTML generated using lcpp2html.