19 lines
445 B
Ada
19 lines
445 B
Ada
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;
|