diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 4cef3c46e..852153147 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -109,12 +109,12 @@ let c_attr (attr : Thir.attribute) : attr =
     | Normal
         {
           item =
-            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None };
+            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None; _ };
           tokens = None;
         } ->
         DocComment { kind = DCKLine; body = symbol }
         (* Looks for `#[doc = "something"]` *)
-    | Normal { item = { args; path; tokens = subtokens }; tokens } ->
+    | Normal { item = { args; path; tokens = subtokens; _ }; tokens } ->
         let args_tokens =
           match args with Delimited { tokens; _ } -> Some tokens | _ -> None
         in
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index 523b2eac3..aefe44096 100644
--- a/frontend/exporter/src/lib.rs
+++ b/frontend/exporter/src/lib.rs
@@ -22,6 +22,7 @@ cfg_feature_rustc! {
     extern crate rustc_abi;
     extern crate rustc_ast;
     extern crate rustc_ast_pretty;
+    extern crate rustc_attr;
     extern crate rustc_data_structures;
     extern crate rustc_driver;
     extern crate rustc_errors;
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 1b5c8ba07..4d12199b9 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -10,7 +10,8 @@ impl std::hash::Hash for DefId {
         let DefId {
             krate,
             path,
-            index: _, // intentionally discarding index
+            index: _,    // intentionally discarding index
+            is_local: _, // intentionally discarding is_local
         } = self;
         krate.hash(state);
         path.hash(state);
@@ -31,6 +32,7 @@ impl<'s, S: BaseState<'s>> SInto<S, DefId> for rustc_hir::def_id::DefId {
                 rustc_hir::def_id::CrateNum::as_u32(self.krate),
                 rustc_hir::def_id::DefIndex::as_u32(self.index),
             ),
+            is_local: self.is_local(),
         }
     }
 }
@@ -107,7 +109,7 @@ pub enum AttrStyle {
 /// Reflects [`rustc_ast::ast::Attribute`]
 #[derive_group(Serializers)]
 #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
-#[args(<'slt, S: BaseState<'slt>>, from: rustc_ast::ast::Attribute, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::Attribute, state: S as gstate)]
 pub struct Attribute {
     pub kind: AttrKind,
     #[map(x.as_usize())]
@@ -116,6 +118,17 @@ pub struct Attribute {
     pub span: Span,
 }
 
+/// Reflects [`rustc_attr::InlineAttr`]
+#[derive_group(Serializers)]
+#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr::InlineAttr, state: S as _s)]
+pub enum InlineAttr {
+    None,
+    Hint,
+    Always,
+    Never,
+}
+
 /// Generic container for decorating items with a type, a span,
 /// attributes and other meta-data.
 #[derive_group(Serializers)]
diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs
index cbb38a802..517ebd8cd 100644
--- a/frontend/exporter/src/types/def_id.rs
+++ b/frontend/exporter/src/types/def_id.rs
@@ -32,7 +32,7 @@ pub struct DisambiguatedDefPathItem {
 
 /// Reflects [`rustc_hir::def_id::DefId`]
 #[derive_group(Serializers)]
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord)]
 #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))]
 pub struct DefId {
     pub krate: String,
@@ -46,6 +46,25 @@ pub struct DefId {
     /// valid only for one Rustc sesssion. Please do not rely on those
     /// indexes unless you cannot do otherwise.
     pub index: (u32, u32),
+    pub is_local: bool,
+}
+
+#[cfg(not(feature = "rustc"))]
+impl std::fmt::Debug for DefId {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        f.debug_struct("DefId")
+            .field("krate", &self.krate)
+            .field("path", &self.path)
+            .finish()
+    }
+}
+
+#[cfg(feature = "rustc")]
+impl std::fmt::Debug for DefId {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        // Use the more legible rustc debug implementation.
+        write!(f, "{:?}", rustc_span::def_id::DefId::from(self))
+    }
 }
 
 /// Reflects [`rustc_hir::definitions::DefPathData`]
diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs
index 0711fc4cc..7e4526e35 100644
--- a/frontend/exporter/src/types/new/full_def.rs
+++ b/frontend/exporter/src/types/new/full_def.rs
@@ -17,6 +17,18 @@ pub struct FullDef {
     pub parent: Option<DefId>,
     #[value(s.base().tcx.def_span(*self).sinto(s))]
     pub span: Span,
+    #[value(s.base().tcx.get_attrs_unchecked(*self).sinto(s))]
+    /// Attributes on this definition, if applicable.
+    pub attributes: Vec<Attribute>,
+    #[value(get_def_visibility(s, *self))]
+    /// Visibility of the definition, for definitions where this makes sense.
+    pub visibility: Option<bool>,
+    #[value(s.base().tcx.as_lang_item(*self).map(|litem| litem.name()).sinto(s))]
+    /// If this definition is a lang item, we store the identifier, e.g. `sized`.
+    pub lang_item: Option<String>,
+    #[value(s.base().tcx.get_diagnostic_name(*self).sinto(s))]
+    /// If this definition is a diagnostic item, we store the identifier, e.g. `box_new`.
+    pub diagnostic_item: Option<String>,
     #[value({
         let state_with_id = State { thir: (), mir: (), owner_id: *self, base: s.base() };
         s.base().tcx.def_kind(*self).sinto(&state_with_id)
@@ -125,6 +137,8 @@ pub enum FullDefKind {
         generics: TyGenerics,
         #[value(get_generic_predicates(s, s.owner_id()))]
         predicates: GenericPredicates,
+        #[value(s.base().tcx.codegen_fn_attrs(s.owner_id()).inline.sinto(s))]
+        inline: InlineAttr,
         #[value(s.base().tcx.fn_sig(s.owner_id()).instantiate_identity().sinto(s))]
         sig: PolyFnSig,
     },
@@ -139,6 +153,8 @@ pub enum FullDefKind {
         generics: TyGenerics,
         #[value(get_generic_predicates(s, s.owner_id()))]
         predicates: GenericPredicates,
+        #[value(s.base().tcx.codegen_fn_attrs(s.owner_id()).inline.sinto(s))]
+        inline: InlineAttr,
         #[value(s.base().tcx.fn_sig(s.owner_id()).instantiate_identity().sinto(s))]
         sig: PolyFnSig,
     },
@@ -310,6 +326,47 @@ impl FullDef {
     }
 }
 
+/// Gets the visibility (`pub` or not) of the definition. Returns `None` for defs that don't have a
+/// meaningful visibility.
+#[cfg(feature = "rustc")]
+fn get_def_visibility<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> Option<bool> {
+    use rustc_hir::def::DefKind::*;
+    let tcx = s.base().tcx;
+    match tcx.def_kind(def_id) {
+        AssocConst
+        | AssocFn
+        | Const
+        | Enum
+        | Field
+        | Fn
+        | ForeignTy
+        | Macro { .. }
+        | Mod
+        | Static { .. }
+        | Struct
+        | Trait
+        | TraitAlias
+        | TyAlias { .. }
+        | Union
+        | Use
+        | Variant => Some(tcx.visibility(def_id).is_public()),
+        // These kinds don't have visibility modifiers (which would cause `visibility` to panic).
+        AnonConst
+        | AssocTy
+        | Closure
+        | ConstParam
+        | Ctor { .. }
+        | ExternCrate
+        | ForeignMod
+        | GlobalAsm
+        | Impl { .. }
+        | InlineConst
+        | LifetimeParam
+        | OpaqueTy
+        | TyParam => None,
+    }
+}
+
 /// This normalizes trait clauses before calling `sinto` on them. This is a bit of a hack required
 /// by charon for now. We can't normalize all clauses as this would lose region information in
 /// outlives clauses.