Function reject_bool_rec_with_swapped_rules

crates/kernel/src/inductive.rs:6752–6832

()

    let rec_block = mk_id("Bool.rec.block");

    // Rebuild recursor type and rule-body domains exactly as `bool_env`
    // does, then swap which Var is returned in each rule.
    let motive_ty = pi(cnst("Bool", &[]), AE::sort(param(0)));
    let minor_true = app(var(0), cnst("Bool.true", &[]));
    let minor_false = app(var(1), cnst("Bool.false", &[]));
    let major_ty = cnst("Bool", &[]);
    let ret = app(var(3), var(0));
    let rec_ty = pi(
      motive_ty.clone(),
      pi(minor_true.clone(), pi(minor_false.clone(), pi(major_ty, ret))),
    );

    // SWAPPED rules: rule 0 returns `h_false` (var 0), rule 1 returns `h_true` (var 1).
    // Canonical: rule 0 returns `h_true` (var 1), rule 1 returns `h_false` (var 0).
    let motive_dom = motive_ty;
    let h_true_dom = minor_true;
    let h_false_dom = minor_false;
    let rule_true_rhs_swapped = lam(
      motive_dom.clone(),
      lam(
        h_true_dom.clone(),
        lam(h_false_dom.clone(), var(0)), // wrong: should be var(1)
      ),
    );
    let rule_false_rhs_swapped = lam(
      motive_dom,
      lam(
        h_true_dom,
        lam(h_false_dom, var(1)), // wrong: should be 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,
        member_idx: 0,
        ty: rec_ty,
        rules: vec![
          super::super::constant::RecRule {
            ctor: (),
            fields: 0,
            rhs: rule_true_rhs_swapped,
          },
          super::super::constant::RecRule {
            ctor: (),
            fields: 0,
            rhs: rule_false_rhs_swapped,
          },