Function n

crates/compile/src/compile/surgery.rs:1121–1123

(s: &str)

/// Both are read off the SOURCE aux recursor's type — the motive binder at
/// `hr.target_motive_pos` has domain `∀ idx…, Ext.{occ} specs… idx… →
/// Sort _` — instantiated with the call site's levels, params, and
/// preceding motives, so the result is expressed in caller terms.
pub fn derive_head_rewrite_app(
  rec_name: &Name,
  rec_levels: &[Level],
  hr: &AuxHeadRewrite,