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;
6
7mod constant_utils;
8mod types;
9
10mod prelude;
11
12pub use prelude::*;
13
14mod sinto;
15mod traits;
16
17pub use hax_adt_into::AdtInto;
18pub use sinto::SInto;
19
20pub mod options {
21    pub use rustc_trait_elaboration::BoundsOptions;
22
23    #[derive(Debug, Default, Clone)]
24    pub struct Options {
25        /// Whether we should evaluate and inline the value of anonymous constants (inline `const {}`
26        /// blocks or advanced constant expressions as in `[T; N+1]`), or refer to them as
27        /// `GlobalName`s.
28        pub inline_anon_consts: bool,
29        /// How to read evaluated constants.
30        pub consts: rustc_const_uneval::Config,
31        /// Whether `Box<T>` is treated as a built-in pointer rather than as a struct.
32        pub treat_box_as_builtin: bool,
33    }
34}
charon_driver/hax/mod.rs

charon_driver/hax/
mod.rs
