charon_driver/hax/types/
mod.rs

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

charon_driver/hax/types/
mod.rs
