Ghost declarations

A ghost declarations annotation may appear anywhere a Rust item may appear, except that only a few kinds of ghost declarations are supported inside function bodies (see Block annotations).

Syntax
GhostDeclarationsAnnotation : /*@ GhostDeclaration * @*/

GhostDeclaration :
      pub GhostDeclaration
   | inductive IDENTIFIER GenericParams ? = |? InductiveConstructor ( | InductiveConstructor )* ;
   | fix IDENTIFIER GenericParams ? ( Params ) ( -> Type )? ( { Expression } | ; )
   | pred IDENTIFIER GenericParams ? ( ( Params ; )? Params ) ( = Assertion )? ;
   | pred_ctor IDENTIFIER GenericParams ? ( Params ) ( ( Params ; )? Params ) = Assertion ;
   | pred GenericParams ? < Type > . IDENTIFIER ( ( ParamNames ; )? ParamNames ) = Assertion ;
   | lem IDENTIFIER GenericParams ? ( Params ) ( -> Type )? LemmaRest
   | fn_type IDENTIFIER GenericParams ? ( Params ) = unsafe fn ( Params ) ( -> Type )? ; req Assertion ; ens Assertion ; on_unwind_ens Assertion ;
   | lem_type IDENTIFIER GenericParams ? ( Params ) = lem ( Params ) ( -> Type )? ; req Assertion ; ens Assertion ;
   | let_lft Lifetime = Expression ;
   | abstract_type IDENTIFIER ;

InductiveConstructor : IDENTIFIER ( ( ( ParamType , )* ParamType ) )?

LemmaRest :
      LemmaSpecification { GhostCommand * }
   | ; LemmaSpecification

LemmaSpecification : nonghost_callers_only? req Assertion ; ens Assertion ;

Params : (( Param , )* Param )?

Param : IDENTIFIER : Type

ParamNames : (( IDENTIFIER , )* IDENTIFIER )?