charon_driver/hax/
mod.rs

1#![allow(rustdoc::private_intra_doc_links)]
2#![allow(clippy::unneeded_struct_pattern, clippy::should_implement_trait)]
3
4mod rustc_utils;
5pub mod state;
6mod utils;
7
8mod constant_utils;
9mod types;
10
11mod index_vec;
12mod prelude;
13
14pub use prelude::*;
15
16mod sinto;
17mod traits;
18
19pub use hax_adt_into::AdtInto;
20pub use sinto::SInto;
21
22pub mod options {
23    pub use rustc_trait_elaboration::BoundsOptions;
24
25    #[derive(Debug, Default, Clone)]
26    pub struct Options {
27        /// Whether we should evaluate and inline the value of anonymous constants (inline `const {}`
28        /// blocks or advanced constant expressions as in `[T; N+1]`), or refer to them as
29        /// `GlobalName`s.
30        pub inline_anon_consts: bool,
31        /// Options related to bounds.
32        pub bounds_options: BoundsOptions,
33    }
34}
charon_driver/hax/mod.rs

charon_driver/hax/
mod.rs
