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 )^?