1package Warn21 is
2
3   type Set is new Integer;
4
5   function "<=" (Left : Set; Right : Set) return Boolean;
6
7   function "=" (Left : Set; Right : Set) return Boolean with
8     Post   => "="'Result = (Left <= Right and Right <= Left);
9
10   procedure Foo;
11
12private
13
14   function "<=" (Left : Set; Right : Set) return Boolean is (True);
15   function "=" (Left : Set; Right : Set) return Boolean is
16      (Left <= Right and Right <= Left);
17
18end Warn21;
19