% @(#) $Id: IntegerConversion.lsl,v 1.2 1997/02/13 00:21:09 leavens Exp $
IntegerConversion(S,T,toT): trait
   assumes Infinite(S), Infinite(T)
   introduces
     toT: S -> T
   asserts \forall s: S
     toT(0) == 0;
     toT(succ(s)) == succ(toT(s))

[Index]

HTML generated using lcpp2html.