On pragma Precondition and types

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

Suppose there is a type T with operations P and F,

   type T is private;

   procedure P (X: in out T);
   function  F (X: T) return Boolean;


I want to add a precondition of P. The precondition
involves F,

   procedure P (X: in out T);
   pragma Precondition (F(X));

   function  F (X: T) return Boolean;


But when the compiler sees the pragma Precondition,
it has not yet seen F.  Therefore, by the principle
of linear reading, the precondition cannot be compiled,
IIUC.

Could there be a rule for pragmas, say, allowing forward
references? Or can these rules be tied to some suitable
constraint syntax?