List of all items

Structs

• int::Int
• prop::Prop

Traits

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

Macros

• assert
• assert_prop
• assume
• coq
• coq::prop
• debug_assert
• fstar
• fstar::prop
• int
• int::implement_abstraction
• int::implement_concretize
• loop_decreases
• loop_invariant
• proc_macros::coq
• proc_macros::coq::prop
• proc_macros::fstar
• proc_macros::fstar::prop
• proc_macros::loop_decreases
• proc_macros::loop_invariant
• proc_macros::proverif
• proc_macros::proverif::prop
• 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
• proc_macros::attributes
• proc_macros::coq::after
• proc_macros::coq::before
• proc_macros::coq::replace
• proc_macros::coq::replace_body
• proc_macros::decreases
• proc_macros::ensures
• proc_macros::exclude
• proc_macros::fstar::after
• proc_macros::fstar::before
• proc_macros::fstar::options
• proc_macros::fstar::postprocess_with
• proc_macros::fstar::replace
• proc_macros::fstar::replace_body
• proc_macros::fstar::smt_pat
• proc_macros::fstar::verification_status
• proc_macros::impl_fn_decoration
• proc_macros::include
• proc_macros::lemma
• proc_macros::opaque
• proc_macros::opaque_type
• proc_macros::process_init
• proc_macros::process_read
• proc_macros::process_write
• proc_macros::protocol_messages
• proc_macros::proverif::after
• proc_macros::proverif::before
• proc_macros::proverif::replace
• proc_macros::proverif::replace_body
• proc_macros::pv_constructor
• proc_macros::pv_handwritten
• proc_macros::refinement_type
• proc_macros::requires
• proc_macros::trait_fn_decoration
• proc_macros::transparent
• 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