Function bool_env

crates/kernel/src/inductive.rs:4558–4675

Build an env with Bool (2 ctors, 0 fields each) and its recursor. Bool : Sort 1 Bool.true : Bool Bool.false : Bool Bool.rec : ∀ (motive : Bool → Sort u) (h₁ : motive Bool.true) (h₂ : motive Bool.false) (t : Bool), motive t

()

      .map(|i| KUniv::param(i, M::meta_field(ix_common::env::Name::anon())))
      .collect();

    // Peel foralls from the domain to detect wrapping.
    // After peeling, the head should be `I_target params idx_args`.
    let wdom = self.whnf(dom)?;
    let mut inner = wdom.clone();
    let mut forall_doms: Vec<KExpr<M>> = Vec::new();

    while let ExprData::All(_, _, fd, fb, _) = inner.data() {
      // Check if this forall's result type (after peeling) has a block
      // inductive as head. If inner itself IS a block inductive app, stop.
      let (h, _) = collect_app_spine(&inner);
      if matches!(h.data(), ExprData::Const(id, _, _)
        if flat.iter().any(|m| m.id.addr == id.addr))
      {
        break;
      }
      forall_doms.push(fd.clone());
      inner = fb.clone();
    }
    let n_xs = checked_usize_to_u64::<M>(
      "generated recursor wrapped-field binder count",
      forall_doms.len(),
    )?;

    // Extract index args from the inner application: `I_target params idx_args`
    let inner_w = self.whnf(&inner)?;
    let (_, inner_args) = collect_app_spine(&inner_w);
    let idx_args: Vec<KExpr<M>> =
      inner_args.iter().skip(target_n_params).cloned().collect();

    // Build the IH core: rec[target] params motives minors indices field
    // All Var references are relative to total_lams (+ n_xs for forall-wrapped case).
    let depth = checked_metadata_sum::<M>(
      "generated recursor induction-hypothesis depth",
      &[total_lams, n_xs],
    )?;
    let n_rec_params_u64 = checked_usize_to_u64::<M>(
      "generated recursor parameter count",
      n_rec_params,
    )?;
    let n_motives_u64 =
      checked_usize_to_u64::<M>("generated recursor motive count", n_motives)?;

    let mut ih = self.intern(KExpr::cnst(peer_rec.clone(), rec_lvls));
    // Apply params
    for pi in 0..n_rec_params {
      let pi =
        checked_usize_to_u64::<M>("generated recursor parameter index", pi)?;
      let pvar = self.intern(KExpr::var(depth - 1 - pi, anon()));
      ih = self.intern(KExpr::app(ih, pvar));
    }
    // Apply motives
    for mi in 0..n_motives {
      let mi =
        checked_usize_to_u64::<M>("generated recursor motive index", mi)?;
      let mvar =
        self.intern(KExpr::var(depth - 1 - n_rec_params_u64 - mi, anon()));
      ih = self.intern(KExpr::app(ih, mvar));