List of all items

Structs

• int::Int
• prop::Prop

Traits

• RefineAs
• Refinement
• int::Abstraction
• int::Concretization
• int::ToInt
• prop::ToProp

Macros

• assert
• assert_prop
• assume
• coq
• coq::prop
• debug_assert
• fstar
• fstar::prop
• int
• loop_decreases
• loop_invariant
• proverif
• proverif::prop

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

• prop::constructors::and
• prop::constructors::eq
• prop::constructors::exists
• prop::constructors::forall
• prop::constructors::from_bool
• prop::constructors::implies
• prop::constructors::ne
• prop::constructors::not
• prop::constructors::or
• prop::exists
• prop::forall
• prop::implies