Keywords

In annotations, these words, in addition to Rust's keywords, are recognized as keywords and cannot be used as identifiers:

_ above abstract_type activating action and_fresh_handle
and_handle any assert assume_correct below box_class by close
consuming_box_pred consuming_handle_pred copred create_box
create_fresh_handle create_handle decreases dispose_box
dup_lem_ptr_chunk emp ens extends fix fix_auto fn_type
forall_ handle handle_pred import_module inductive inv leak
lem lem_auto lem_type let_lft merge_fractions
nonghost_callers_only on_unwind_ens open perform_action permbased pred
pred_ctor pred_fam pred_fam_inst preserved_by produce_fn_ptr_chunk
produce_lem_ptr_chunk producing_box_pred producing_fresh_handle_pred
producing_handle_pred req require_module split_fraction terminates
truncating type_pred_decl type_pred_def typedef typeid
unloadable_module

These are the additional operators recognized inside annotations:

&*& |-> |-?-> @