Use of expression function in protected type

[Simon Wright <simon@pushface.org>]

Is it permissible to use an expression function as the completion of a
protected function? (GNAT thinks so).

   protected Button
   is
      function Current_Index return Interval_Index;
   private
      Index : Interval_Index := 0;
      procedure Handler;
      pragma Attach_Handler (Handler, Ada.Interrupts.Names.EXTI0_IRQ);
   end Button;

and then

   protected body Button is
      function Current_Index return Interval_Index is (Index); -- <<<<<<<<
      procedure Handler is
      begin
         HAL_GPIO_EXTI_IRQHandler (16#0001#);
         Index := Index + 1;
      end Handler;
   end Button;

ARM 6.1(30) distinguishes an expression_function_declaration from a
subprogram_declaration.

6.8(4) allows an expression_function_declaration to be a completion.

9.4(8) says a protected_operation_item can be, inter alia, a
subprogram_declaration or a subprogram body. (subprogram_declaration?
how can that be?)