lean_rs_host/host/
declaration_search.rs

1//! Structured declaration search bridge for the bundled host shim.
2//!
3//! Lean owns the environment scan because it can inspect `ConstantInfo`
4//! without rendering types. Rust only encodes the request policy and decodes
5//! bounded rows plus fanout facts.
6
7use lean_rs::abi::nat;
8use lean_rs::abi::structure::{alloc_ctor_with_objects, take_ctor_objects, view};
9use lean_rs::abi::traits::{IntoLean, LeanAbi, TryFromLean, conversion_error, sealed};
10use lean_rs::{LeanRuntime, Obj};
11
12use crate::host::session::{LeanDeclarationFilter, LeanSourceRange};
13
14#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
15pub enum DeclarationNameMatch {
16    #[default]
17    Contains,
18    Suffix,
19}
20
21#[derive(Clone, Copy, Debug, Eq, PartialEq)]
22pub enum DeclarationSearchScope {
23    Namespace,
24    Module,
25}
26
27#[derive(Clone, Debug, Eq, PartialEq)]
28pub struct DeclarationSearchBias {
29    pub scope: DeclarationSearchScope,
30    pub prefix: String,
31    pub strict: bool,
32    pub weight: i32,
33}
34
35#[derive(Clone, Debug, Eq, PartialEq)]
36pub struct DeclarationSearchRequest {
37    pub name_fragment: Option<String>,
38    pub name_match: DeclarationNameMatch,
39    pub kind: Option<String>,
40    pub required_constants: Vec<String>,
41    pub conclusion_head: Option<String>,
42    pub scope_biases: Vec<DeclarationSearchBias>,
43    pub limit: usize,
44    pub filter: LeanDeclarationFilter,
45    pub include_source: bool,
46}
47
48impl DeclarationSearchRequest {
49    #[must_use]
50    pub fn new(name_fragment: impl Into<String>) -> Self {
51        Self {
52            name_fragment: Some(name_fragment.into()),
53            name_match: DeclarationNameMatch::Contains,
54            kind: None,
55            required_constants: Vec::new(),
56            conclusion_head: None,
57            scope_biases: Vec::new(),
58            limit: 20,
59            filter: LeanDeclarationFilter {
60                include_private: false,
61                include_generated: false,
62                include_internal: false,
63            },
64            include_source: true,
65        }
66    }
67}
68
69#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
70pub struct DeclarationFlags {
71    pub is_private: bool,
72    pub is_generated: bool,
73    pub is_internal: bool,
74}
75
76#[derive(Clone, Debug, Eq, PartialEq)]
77pub struct DeclarationSearchRow {
78    pub name: String,
79    pub kind: String,
80    pub module: Option<String>,
81    pub source: Option<LeanSourceRange>,
82    pub match_reason: String,
83    pub score: i32,
84    pub rank: usize,
85    pub flags: DeclarationFlags,
86}
87
88#[derive(Clone, Debug, Eq, PartialEq)]
89pub struct DeclarationSearchPruning {
90    pub stage: String,
91    pub reason: String,
92    pub count: usize,
93}
94
95#[derive(Clone, Debug, Default, Eq, PartialEq)]
96pub struct DeclarationSearchTimings {
97    pub scan_micros: u64,
98    pub rank_micros: u64,
99    pub source_micros: u64,
100}
101
102#[derive(Clone, Debug, Default, Eq, PartialEq)]
103pub struct LeanDerivedWorkFacts {
104    pub source_range_lookups: u64,
105    pub docstring_lookups: u64,
106    pub raw_type_renderings: u64,
107    pub pretty_prints: u64,
108    pub proof_search_fact_collections: u64,
109    pub simp_extension_lookups: u64,
110    pub parser_elaborator_runs: u64,
111    pub module_snapshot_builds: u64,
112    pub lazy_discr_tree_import_initialization_observed: bool,
113}
114
115#[derive(Clone, Debug, Default, Eq, PartialEq)]
116pub struct DeclarationSearchFacts {
117    pub declarations_scanned: usize,
118    pub after_name_filter: usize,
119    pub after_kind_filter: usize,
120    pub after_required_constants_filter: usize,
121    pub after_conclusion_filter: usize,
122    pub after_scope_filter: usize,
123    pub source_lookups: usize,
124    pub broad_pruning: Vec<DeclarationSearchPruning>,
125    pub truncated: bool,
126    pub timings: DeclarationSearchTimings,
127    pub derived_work: LeanDerivedWorkFacts,
128}
129
130#[derive(Clone, Debug, Eq, PartialEq)]
131pub struct DeclarationSearchResult {
132    pub declarations: Vec<DeclarationSearchRow>,
133    pub truncated: bool,
134    pub facts: DeclarationSearchFacts,
135}
136
137#[derive(Clone, Copy, Debug, Eq, PartialEq)]
138#[allow(
139    clippy::struct_excessive_bools,
140    reason = "field-selection flags mirror the Lean request shape and are clearer than five tiny enums"
141)]
142pub struct DeclarationInspectionFields {
143    pub source: bool,
144    pub statement: bool,
145    pub docstring: bool,
146    pub attributes: bool,
147    pub flags: bool,
148    /// Render `statement` notation-aware (`pp.universes false`) when `true`,
149    /// falling back to the raw term if the pretty-printer cannot render it;
150    /// the fully-elaborated raw form when `false`.
151    pub statement_pretty: bool,
152    /// Include proof-search-oriented facts such as simp/rw/instance/class.
153    /// Defaults off because these facts may touch persistent extensions and
154    /// lazy derived search indexes.
155    pub proof_search: bool,
156}
157
158impl Default for DeclarationInspectionFields {
159    fn default() -> Self {
160        Self {
161            source: true,
162            statement: true,
163            docstring: true,
164            attributes: true,
165            flags: true,
166            statement_pretty: true,
167            proof_search: false,
168        }
169    }
170}
171
172#[derive(Clone, Copy, Debug, Eq, PartialEq)]
173pub struct DeclarationInspectionBudgets {
174    pub per_field_bytes: u32,
175    pub total_bytes: u32,
176}
177
178impl Default for DeclarationInspectionBudgets {
179    fn default() -> Self {
180        Self {
181            per_field_bytes: 8 * 1024,
182            total_bytes: 64 * 1024,
183        }
184    }
185}
186
187#[derive(Clone, Debug, Eq, PartialEq)]
188pub struct DeclarationInspectionRequest {
189    pub name: String,
190    pub fields: DeclarationInspectionFields,
191    pub budgets: DeclarationInspectionBudgets,
192}
193
194impl DeclarationInspectionRequest {
195    #[must_use]
196    pub fn new(name: impl Into<String>) -> Self {
197        Self {
198            name: name.into(),
199            fields: DeclarationInspectionFields::default(),
200            budgets: DeclarationInspectionBudgets::default(),
201        }
202    }
203}
204
205#[derive(Clone, Debug, Eq, PartialEq)]
206pub struct DeclarationRenderedInfo {
207    pub value: String,
208    pub truncated: bool,
209}
210
211#[derive(Clone, Debug, Default, Eq, PartialEq)]
212#[allow(
213    clippy::struct_excessive_bools,
214    reason = "proof-search booleans are independent inspection facts, not control-flow state"
215)]
216pub struct DeclarationProofSearchFacts {
217    pub computed: bool,
218    pub unavailable_reason: Option<String>,
219    pub is_simp: bool,
220    pub is_rw_candidate: bool,
221    pub is_instance: bool,
222    pub is_class: bool,
223    pub class_name: Option<String>,
224}
225
226#[derive(Clone, Debug, Eq, PartialEq)]
227pub struct DeclarationInspection {
228    pub name: String,
229    pub kind: String,
230    pub module: Option<String>,
231    pub source: Option<LeanSourceRange>,
232    pub statement: Option<DeclarationRenderedInfo>,
233    pub docstring: Option<DeclarationRenderedInfo>,
234    pub attributes: Vec<String>,
235    pub proof_search: DeclarationProofSearchFacts,
236    pub flags: DeclarationFlags,
237    pub derived_work: LeanDerivedWorkFacts,
238    /// Rendering that produced `statement`: `Some(true)` = pretty, `Some(false)`
239    /// = raw, `None` when no statement was requested.
240    pub statement_pretty: Option<bool>,
241}
242
243#[derive(Clone, Debug, Eq, PartialEq)]
244pub enum DeclarationInspectionResult {
245    Found { declaration: Box<DeclarationInspection> },
246    NotFound { name: String },
247    Unsupported,
248}
249
250impl<'lean> IntoLean<'lean> for DeclarationNameMatch {
251    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
252        match self {
253            Self::Contains => nat::from_usize(runtime, 0),
254            Self::Suffix => nat::from_usize(runtime, 1),
255        }
256    }
257}
258
259impl<'lean> IntoLean<'lean> for DeclarationSearchScope {
260    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
261        match self {
262            Self::Namespace => nat::from_usize(runtime, 0),
263            Self::Module => nat::from_usize(runtime, 1),
264        }
265    }
266}
267
268fn nat_from_bool(runtime: &LeanRuntime, value: bool) -> Obj<'_> {
269    nat::from_usize(runtime, usize::from(value))
270}
271
272fn bool_from_nat(obj: Obj<'_>) -> lean_rs::LeanResult<bool> {
273    Ok(nat::try_to_usize(obj)? != 0)
274}
275
276impl<'lean> IntoLean<'lean> for DeclarationSearchBias {
277    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
278        alloc_ctor_with_objects(
279            runtime,
280            0,
281            [
282                self.scope.into_lean(runtime),
283                self.prefix.into_lean(runtime),
284                nat_from_bool(runtime, self.strict),
285                self.weight.to_string().into_lean(runtime),
286            ],
287        )
288    }
289}
290
291impl<'lean> IntoLean<'lean> for DeclarationSearchRequest {
292    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
293        alloc_ctor_with_objects(
294            runtime,
295            0,
296            [
297                self.name_fragment.into_lean(runtime),
298                self.name_match.into_lean(runtime),
299                self.kind.into_lean(runtime),
300                self.required_constants.into_lean(runtime),
301                self.conclusion_head.into_lean(runtime),
302                self.scope_biases.into_lean(runtime),
303                nat::from_usize(runtime, self.limit),
304                self.filter.into_lean(runtime),
305                nat_from_bool(runtime, self.include_source),
306            ],
307        )
308    }
309}
310
311impl<'lean> IntoLean<'lean> for DeclarationInspectionFields {
312    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
313        alloc_ctor_with_objects(
314            runtime,
315            0,
316            [
317                nat_from_bool(runtime, self.source),
318                nat_from_bool(runtime, self.statement),
319                nat_from_bool(runtime, self.docstring),
320                nat_from_bool(runtime, self.attributes),
321                nat_from_bool(runtime, self.flags),
322                nat_from_bool(runtime, self.statement_pretty),
323                nat_from_bool(runtime, self.proof_search),
324            ],
325        )
326    }
327}
328
329impl<'lean> IntoLean<'lean> for DeclarationInspectionBudgets {
330    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
331        alloc_ctor_with_objects(
332            runtime,
333            0,
334            [
335                nat::from_usize(runtime, self.per_field_bytes as usize),
336                nat::from_usize(runtime, self.total_bytes as usize),
337            ],
338        )
339    }
340}
341
342impl<'lean> IntoLean<'lean> for DeclarationInspectionRequest {
343    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
344        alloc_ctor_with_objects(
345            runtime,
346            0,
347            [
348                self.name.into_lean(runtime),
349                self.fields.into_lean(runtime),
350                self.budgets.into_lean(runtime),
351            ],
352        )
353    }
354}
355
356impl sealed::SealedAbi for DeclarationInspectionRequest {}
357
358impl<'lean> LeanAbi<'lean> for DeclarationInspectionRequest {
359    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
360
361    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
362        self.into_lean(runtime).into_raw()
363    }
364
365    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
366        Err(conversion_error(
367            "DeclarationInspectionRequest cannot decode a Lean call result; it is an argument-only type",
368        ))
369    }
370}
371
372impl sealed::SealedAbi for &DeclarationInspectionRequest {}
373
374impl<'lean> LeanAbi<'lean> for &DeclarationInspectionRequest {
375    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
376
377    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
378        self.clone().into_lean(runtime).into_raw()
379    }
380
381    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
382        Err(conversion_error(
383            "&DeclarationInspectionRequest cannot decode a Lean call result; use DeclarationInspectionRequest for owned values",
384        ))
385    }
386}
387
388impl sealed::SealedAbi for DeclarationSearchRequest {}
389
390impl<'lean> LeanAbi<'lean> for DeclarationSearchRequest {
391    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
392
393    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
394        self.into_lean(runtime).into_raw()
395    }
396
397    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
398        Err(conversion_error(
399            "DeclarationSearchRequest cannot decode a Lean call result; it is an argument-only type",
400        ))
401    }
402}
403
404impl sealed::SealedAbi for &DeclarationSearchRequest {}
405
406impl<'lean> LeanAbi<'lean> for &DeclarationSearchRequest {
407    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
408
409    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
410        self.clone().into_lean(runtime).into_raw()
411    }
412
413    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
414        Err(conversion_error(
415            "&DeclarationSearchRequest cannot decode a Lean call result; use DeclarationSearchRequest for owned values",
416        ))
417    }
418}
419
420impl<'lean> TryFromLean<'lean> for DeclarationFlags {
421    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
422        let [is_private, is_generated, is_internal] = take_ctor_objects::<3>(obj, 0, "DeclarationFlags")?;
423        Ok(Self {
424            is_private: bool_from_nat(is_private)?,
425            is_generated: bool_from_nat(is_generated)?,
426            is_internal: bool_from_nat(is_internal)?,
427        })
428    }
429}
430
431impl<'lean> TryFromLean<'lean> for DeclarationSearchRow {
432    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
433        let [name, kind, module, source, match_reason, score, rank, flags] =
434            take_ctor_objects::<8>(obj, 0, "DeclarationSearchRow")?;
435        Ok(Self {
436            name: String::try_from_lean(name)?,
437            kind: String::try_from_lean(kind)?,
438            module: Option::<String>::try_from_lean(module)?,
439            source: Option::<LeanSourceRange>::try_from_lean(source)?,
440            match_reason: String::try_from_lean(match_reason)?,
441            score: String::try_from_lean(score)?
442                .parse()
443                .map_err(|_| conversion_error("score does not fit i32"))?,
444            rank: nat::try_to_usize(rank)?,
445            flags: DeclarationFlags::try_from_lean(flags)?,
446        })
447    }
448}
449
450impl<'lean> TryFromLean<'lean> for DeclarationSearchPruning {
451    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
452        let [stage, reason, count] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchPruning")?;
453        Ok(Self {
454            stage: String::try_from_lean(stage)?,
455            reason: String::try_from_lean(reason)?,
456            count: nat::try_to_usize(count)?,
457        })
458    }
459}
460
461impl<'lean> TryFromLean<'lean> for DeclarationSearchTimings {
462    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
463        let [scan_micros, rank_micros, source_micros] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchTimings")?;
464        Ok(Self {
465            scan_micros: nat::try_to_u64(scan_micros)?,
466            rank_micros: nat::try_to_u64(rank_micros)?,
467            source_micros: nat::try_to_u64(source_micros)?,
468        })
469    }
470}
471
472impl<'lean> TryFromLean<'lean> for LeanDerivedWorkFacts {
473    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
474        let [
475            source_range_lookups,
476            docstring_lookups,
477            raw_type_renderings,
478            pretty_prints,
479            proof_search_fact_collections,
480            simp_extension_lookups,
481            parser_elaborator_runs,
482            module_snapshot_builds,
483            lazy_discr_tree_import_initialization_observed,
484        ] = take_ctor_objects::<9>(obj, 0, "DerivedWorkFacts")?;
485        Ok(Self {
486            source_range_lookups: nat::try_to_u64(source_range_lookups)?,
487            docstring_lookups: nat::try_to_u64(docstring_lookups)?,
488            raw_type_renderings: nat::try_to_u64(raw_type_renderings)?,
489            pretty_prints: nat::try_to_u64(pretty_prints)?,
490            proof_search_fact_collections: nat::try_to_u64(proof_search_fact_collections)?,
491            simp_extension_lookups: nat::try_to_u64(simp_extension_lookups)?,
492            parser_elaborator_runs: nat::try_to_u64(parser_elaborator_runs)?,
493            module_snapshot_builds: nat::try_to_u64(module_snapshot_builds)?,
494            lazy_discr_tree_import_initialization_observed: bool_from_nat(
495                lazy_discr_tree_import_initialization_observed,
496            )?,
497        })
498    }
499}
500
501impl<'lean> TryFromLean<'lean> for DeclarationSearchFacts {
502    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
503        let [
504            declarations_scanned,
505            after_name_filter,
506            after_kind_filter,
507            after_required_constants_filter,
508            after_conclusion_filter,
509            after_scope_filter,
510            source_lookups,
511            broad_pruning,
512            truncated,
513            timings,
514            derived_work,
515        ] = take_ctor_objects::<11>(obj, 0, "DeclarationSearchFacts")?;
516        Ok(Self {
517            declarations_scanned: nat::try_to_usize(declarations_scanned)?,
518            after_name_filter: nat::try_to_usize(after_name_filter)?,
519            after_kind_filter: nat::try_to_usize(after_kind_filter)?,
520            after_required_constants_filter: nat::try_to_usize(after_required_constants_filter)?,
521            after_conclusion_filter: nat::try_to_usize(after_conclusion_filter)?,
522            after_scope_filter: nat::try_to_usize(after_scope_filter)?,
523            source_lookups: nat::try_to_usize(source_lookups)?,
524            broad_pruning: Vec::<DeclarationSearchPruning>::try_from_lean(broad_pruning)?,
525            truncated: bool_from_nat(truncated)?,
526            timings: DeclarationSearchTimings::try_from_lean(timings)?,
527            derived_work: LeanDerivedWorkFacts::try_from_lean(derived_work)?,
528        })
529    }
530}
531
532impl<'lean> TryFromLean<'lean> for DeclarationSearchResult {
533    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
534        let [declarations, truncated, facts] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchResult")?;
535        Ok(Self {
536            declarations: Vec::<DeclarationSearchRow>::try_from_lean(declarations)?,
537            truncated: bool_from_nat(truncated)?,
538            facts: DeclarationSearchFacts::try_from_lean(facts)?,
539        })
540    }
541}
542
543impl<'lean> TryFromLean<'lean> for DeclarationRenderedInfo {
544    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
545        let [value, truncated] = take_ctor_objects::<2>(obj, 0, "DeclarationRenderedInfo")?;
546        Ok(Self {
547            value: String::try_from_lean(value)?,
548            truncated: bool_from_nat(truncated)?,
549        })
550    }
551}
552
553impl<'lean> TryFromLean<'lean> for DeclarationProofSearchFacts {
554    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
555        let [
556            computed,
557            unavailable_reason,
558            is_simp,
559            is_rw_candidate,
560            is_instance,
561            is_class,
562            class_name,
563        ] = take_ctor_objects::<7>(obj, 0, "DeclarationProofSearchFacts")?;
564        Ok(Self {
565            computed: bool_from_nat(computed)?,
566            unavailable_reason: Option::<String>::try_from_lean(unavailable_reason)?,
567            is_simp: bool_from_nat(is_simp)?,
568            is_rw_candidate: bool_from_nat(is_rw_candidate)?,
569            is_instance: bool_from_nat(is_instance)?,
570            is_class: bool_from_nat(is_class)?,
571            class_name: Option::<String>::try_from_lean(class_name)?,
572        })
573    }
574}
575
576impl<'lean> TryFromLean<'lean> for DeclarationInspection {
577    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
578        let [
579            name,
580            kind,
581            module,
582            source,
583            statement,
584            docstring,
585            attributes,
586            proof_search,
587            flags,
588            derived_work,
589            statement_rendering,
590        ] = take_ctor_objects::<11>(obj, 0, "DeclarationInspection")?;
591        // `statementRendering : Option Nat` (1 = pretty, 0 = raw) → Option<bool>.
592        let statement_pretty = match view(&statement_rendering).sum_tag()? {
593            0 => None,
594            1 => {
595                let [nat] = take_ctor_objects::<1>(statement_rendering, 1, "DeclarationInspection.statementRendering")?;
596                Some(bool_from_nat(nat)?)
597            }
598            other => {
599                return Err(conversion_error(format!(
600                    "expected Lean Option ctor (tag 0..=1) for statementRendering, found tag {other}"
601                )));
602            }
603        };
604        Ok(Self {
605            name: String::try_from_lean(name)?,
606            kind: String::try_from_lean(kind)?,
607            module: Option::<String>::try_from_lean(module)?,
608            source: Option::<LeanSourceRange>::try_from_lean(source)?,
609            statement: Option::<DeclarationRenderedInfo>::try_from_lean(statement)?,
610            docstring: Option::<DeclarationRenderedInfo>::try_from_lean(docstring)?,
611            attributes: Vec::<String>::try_from_lean(attributes)?,
612            proof_search: DeclarationProofSearchFacts::try_from_lean(proof_search)?,
613            flags: DeclarationFlags::try_from_lean(flags)?,
614            derived_work: LeanDerivedWorkFacts::try_from_lean(derived_work)?,
615            statement_pretty,
616        })
617    }
618}
619
620impl<'lean> TryFromLean<'lean> for DeclarationInspectionResult {
621    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
622        match view(&obj).sum_tag()? {
623            0 => {
624                let [declaration] = take_ctor_objects::<1>(obj, 0, "DeclarationInspectionResult::found")?;
625                Ok(Self::Found {
626                    declaration: Box::new(DeclarationInspection::try_from_lean(declaration)?),
627                })
628            }
629            1 => {
630                let [name] = take_ctor_objects::<1>(obj, 1, "DeclarationInspectionResult::notFound")?;
631                Ok(Self::NotFound {
632                    name: String::try_from_lean(name)?,
633                })
634            }
635            2 => {
636                let [] = take_ctor_objects::<0>(obj, 2, "DeclarationInspectionResult::unsupported")?;
637                Ok(Self::Unsupported)
638            }
639            other => Err(conversion_error(format!(
640                "expected Lean DeclarationInspectionResult ctor (tag 0..=2), found tag {other}"
641            ))),
642        }
643    }
644}
lean_rs_host/host/declaration_search.rs

lean_rs_host/host/
declaration_search.rs
