Function check_nat_rec

crates/kernel/src/inductive.rs:4865–4870

()

    // Signature-based match for aux recursors.
    //
    // Nested auxiliaries can contain several recursors with the same external
    // major head (for example multiple `List` auxes with different element
    // types). Matching only by `ind_addr` picks the first such recursor.
    // Matching primarily by the stored recursor's block position is also too
    // brittle: the compiled recursor block is sorted as recursor constants,
    // while generation is ordered by the flat inductive layout. Select by the
    // extracted major premise domain first, then keep the old positional and
    // address lookups as fixture fallbacks.
    let stored_pos: Option<usize> = self