charon_driver/hax/types/
mod.rs

1mod adt;
2mod def_id;
3mod mir;
4mod new;
5mod predicates;
6mod traits;
7mod ty;
8mod vars;
9
10pub use adt::*;
11pub use def_id::*;
12pub use mir::*;
13pub use new::*;
14pub use predicates::*;
15pub use traits::*;
16pub use ty::*;
17pub use vars::*;
18
19use crate::hax::prelude::*;
20use crate::hax::sinto_todo;
21
22sinto_reexport!(rustc_span::Span);
23
24pub use rustc_span::Spanned;
25impl<'s, S: UnderOwnerState<'s>, T: SInto<S, U>, U> SInto<S, Spanned<U>> for Spanned<T> {
26    fn sinto<'a>(&self, s: &S) -> Spanned<U> {
27        Spanned {
28            node: self.node.sinto(s),
29            span: self.span,
30        }
31    }
32}
33
34sinto_todo!(rustc_span, ErrorGuaranteed);
35
36/// Reflects [`rustc_span::symbol::Ident`]
37pub type Ident = (Symbol, Span);
38impl<'tcx, S: BaseState<'tcx>> SInto<S, Ident> for rustc_span::symbol::Ident {
39    fn sinto(&self, s: &S) -> Ident {
40        (self.name.sinto(s), self.span.sinto(s))
41    }
42}
charon_driver/hax/types/mod.rs

charon_driver/hax/types/
mod.rs
