Function bad_induct_too_few_params

crates/kernel/src/tutorial/inductive.rs:121–171

()

    let mut env = KEnv::<Meta>::new();
    let block_id = mk_id("inductTooFewParams");
    let rec_id = mk_id("inductTooFewParams.rec");
    env.insert(
      block_id.clone(),
      KConst::Indc {
        name: mk_name("inductTooFewParams"),
        level_params: vec![],
        lvls: 0,
        params: 2, // claims 2 params
        indices: 0,
        is_unsafe: false,
        block: block_id.clone(),
        member_idx: 0,
        ty: pi(sort0(), sort0()), // only 1 arrow — Prop → Prop
        ctors: vec![],
        lean_all: vec![block_id.clone()],
      },
    );
    // Minimal recursor
    let rec_ty = npi(
      "motive",
      pi(pi(sort0(), sort0()), sort(param(0))),
      npi("t", pi(sort0(), sort0()), app(var(1), var(0))),
    );
    env.insert(
      rec_id.clone(),
      KConst::Recr {
        name: mk_name("inductTooFewParams.rec"),
        level_params: vec![mk_name("u")],
        k: false,
        is_unsafe: false,
        lvls: 1,
        params: 2,
        indices: 0,
        motives: 1,
        minors: 0,
        block: block_id.clone(),
        member_idx: 0,
        ty: rec_ty,
        rules: vec![],
        lean_all: vec![block_id.clone()],
      },
    );
    env.blocks.insert(block_id.clone(), vec![block_id.clone(), rec_id]);
    check_rejects(&mut env, &block_id);
  }

  /// indNeg: classic negative recursive occurrence: (I → I) → I
  #[test]
  fn bad_induct_negative_occurrence() {
    let mut env = KEnv::<Meta>::new();
    let n = "indNeg";
    let block_id = mk_id(n);
    let ctor_id = mk_id("indNeg.mk");
    let rec_id = mk_id("indNeg.rec");