Function build_test_env

crates/compile/src/compile/surgery.rs:1208–1282

Helper: build a minimal Lean environment with mutual inductives.

(
    names: &[&str],
    ctor_counts: &[usize],
  )

       occurrence supplies {}",
      hr.target_rec.pretty(),
      needed,
      occ_levels.len()
    ));
  };
  Ok((target_levels, sig.specs.clone()))
}

fn source_minor_type(
  rec: &RecursorVal,
  rec_levels: &[Level],
  params: &[LeanExpr],
  motives: &[LeanExpr],
  minors: &[LeanExpr],
  src_minor_idx: usize,
) -> Option<LeanExpr> {
  let mut cur = subst_levels(&rec.cnst.typ, &rec.cnst.level_params, rec_levels);
  for arg in
    params.iter().chain(motives.iter()).chain(minors.iter().take(src_minor_idx))
  {
    match cur.as_data() {
      ExprData::ForallE(_, _, body, _, _) => {
        // `instantiate_rev`, not `instantiate1`: call-site args may carry
        // loose BVars into the caller's telescope (rec applications under
        // binders, e.g. `.brecOn_N.go` bodies) and must be lifted when
        // substituted under the type's remaining binders.
        cur = instantiate_rev(body, std::slice::from_ref(arg));
      },
      _ => return None,
    }
  }
  match cur.as_data() {
    ExprData::ForallE(_, dom, _, _, _) => Some(consume_type_annotations(dom)),
    _ => None,
  }
}

fn peel_binders(
  mut cur: LeanExpr,
  n: usize,
  prefix: &str,
  offset: usize,
) -> Option<(Vec<LocalDecl>, Vec<LeanExpr>, LeanExpr)> {
  let mut decls = Vec::with_capacity(n);
  let mut fvars = Vec::with_capacity(n);
  for i in 0..n {
    match cur.as_data() {
      ExprData::ForallE(name, dom, body, bi, _) => {
        let (fv_name, fv) = fresh_fvar(prefix, offset + i);
        let decl = LocalDecl {
          fvar_name: fv_name,
          binder_name: name.clone(),
          domain: consume_type_annotations(dom),
          info: bi.clone(),
        };
        cur = instantiate1(body, &fv);
        fvars.push(fv);
        decls.push(decl);
      },