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