List of all items
Macros
- coq_expr
- coq_prop_expr
- coq_unsafe_expr
- fstar_expr
- fstar_prop_expr
- fstar_unsafe_expr
- identity_proc_macro_attribute
- int
- loop_decreases
- loop_invariant
- proverif_expr
- proverif_prop_expr
- proverif_unsafe_expr
Attribute Macros
- attributes
- coq_after
- coq_before
- coq_replace
- coq_replace_body
- decreases
- ensures
- exclude
- fstar_after
- fstar_before
- fstar_options
- fstar_postprocess_with
- fstar_replace
- fstar_replace_body
- fstar_smt_pat
- fstar_verification_status
- impl_fn_decoration
- include
- lemma
- opaque
- opaque_type
- process_init
- process_read
- process_write
- protocol_messages
- proverif_after
- proverif_before
- proverif_replace
- proverif_replace_body
- pv_constructor
- pv_handwritten
- refinement_type
- requires
- trait_fn_decoration
- transparent
Functions
- hax_paths::expect_simple_path
- hax_paths::expects_hax_path
- hax_paths::expects_order
- hax_paths::expects_path_decoration
- hax_paths::expects_refine
- not_field_attribute
- not_hax_attribute
- unsafe_expr