Docs.rs
  • hax-lib-0.3.1
    • hax-lib 0.3.1
    • Permalink
    • Docs.rs crate page
    • Apache-2.0
    • Links
    • Homepage
    • Repository
    • crates.io
    • Source
    • Owners
    • franziskuskiefer
    • github:cryspen:tools
    • Dependencies
      • hax-lib-macros =0.3.1 normal optional
      • num-bigint ^0.4 normal
      • num-traits ^0.2 normal
    • Versions
    • 25.37% of the crate is documented
  • Platform
    • i686-pc-windows-msvc
    • i686-unknown-linux-gnu
    • x86_64-apple-darwin
    • x86_64-pc-windows-msvc
    • x86_64-unknown-linux-gnu
  • Feature flags
  • docs.rs
    • About docs.rs
    • Privacy policy
  • Rust
    • Rust website
    • The Book
    • Standard Library API Reference
    • Rust by Example
    • The Cargo Guide
    • Clippy Documentation

hax_lib0.3.1

Crate Items

  • Macros
  • Structs
  • Traits
  • Functions
  • Attribute Macros

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