It should be possible to have pragmas inside record declarations

[lukaszcz]

The following

type Pr (A B : Type) := mkPr {
     {-# inline: true #-}
     pfst : A;
     psnd : B
};

currently gives an error

  |
6 |      {-# inline: true #-}
  |      ^
unexpected '{'
expecting <identifier>, builtin, syntax, or }

Instead, the pragma should be accepted and associated with the generated record projection.

This would be useful to have for the Isabelle translation, to be able to indicate that certain functions in a trait should be translated to specific Isabelle operators.