Function nested_tree_rec_binder_count

crates/kernel/src/inductive.rs:5328–5368

()

    );

    // Bool.rec rules — use actual domain types from recursor type
    let motive_dom = motive_ty;
    let h_true_dom = minor_true;
    let h_false_dom = minor_false;
    // Rule 0 (Bool.true, 0 fields): λ (motive) (h_true) (h_false), h_true
    let rule_true_rhs = lam(
      motive_dom.clone(),
      lam(h_true_dom.clone(), lam(h_false_dom.clone(), var(1))),
    );
    // Rule 1 (Bool.false, 0 fields): λ (motive) (h_true) (h_false), h_false
    let rule_false_rhs =
      lam(motive_dom, lam(h_true_dom, lam(h_false_dom, var(0))));

    env.insert(
      mk_id("Bool.rec"),
      KConst::Recr {
        name: (),
        level_params: (),
        k: false,
        is_unsafe: false,
        lvls: 1,
        params: 0,
        indices: 0,
        motives: 1,
        minors: 2,
        block: rec_block.clone(),
        member_idx: 0,
        ty: rec_ty,
        rules: vec![
          super::super::constant::RecRule {
            ctor: (),
            fields: 0,
            rhs: rule_true_rhs,
          },
          super::super::constant::RecRule {
            ctor: (),
            fields: 0,
            rhs: rule_false_rhs,
          },
        ],
        lean_all: (),
      },
    );