% @(#)$Id: Between.lsl,v 1.3 1995/11/09 21:21:36 leavens Exp $
Between(T): trait
  assumes PartialOrder
  introduces
    between, strictly_between: T, T, T -> Bool
    between, strictly_between: T, T, T, T -> Bool
  asserts
    \forall w, x, y, z: T
      between(x,y,z) == x <= y /\ y <= z;
      between(w,x,y,z) == w <= x /\ x <= y /\ y <= z;
      strictly_between(x,y,z) == x < y /\ y < z;
      strictly_between(w,x,y,z) == w < x /\ x < y /\ y < z;
      strictly_between(w,x,y,z) == w < x /\ x < y /\ y < z;

[Index]

HTML generated using lcpp2html.