blob: adf9b92121827ac9ea46ad6b9706f373c34eca9f [file] [log] [blame]
package Assert2
with SPARK_Mode
is
type Living is new Integer;
function Is_Martian (Unused : Living) return Boolean is (False);
function Is_Green (Unused : Living) return Boolean is (True);
pragma Assert
(for all M in Living => (if Is_Martian (M) then Is_Green (M)));
pragma Assert
(for all M in Living => (if Is_Martian (M) then not Is_Green (M)));
procedure Dummy;
end Assert2;