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 *}
|;
LemmaSpecificationLemmaSpecification :
nonghost_callers_only
?req
Assertion;
ens
Assertion;
Params : (( Param
,
)* Param )?Param : IDENTIFIER
:
TypeParamNames : (( IDENTIFIER
,
)* IDENTIFIER )?