Function is_extractable 

pub fn is_extractable(ctx: &Context, name: &str) -> bool

Whether name extracts to self-contained Rust: a constructor of an emittable inductive, an emittable inductive (has constructors) or mapped primitive, or a definition whose body only references extractable things. Axioms / declarations / tactics (no extractable body, e.g. syn_diag, try_auto) are NOT extractable — extracting them would emit Rust referencing undefined symbols.