Function bad_induct_in_index

crates/kernel/src/tutorial/inductive.rs:1208–1289

()

        lvls: 0,
        induct: block_id.clone(),
        cidx: 0,
        params: 0,
        fields: 0,
        ty: i_i_aprop,
      },
    );

    let rec_ty = ipi(
      "motive",
      npi("x", sort0(), pi(app(cnst(n, &[]), var(0)), sort0())),
      npi(
        "x",
        sort0(),
        npi("t", app(cnst(n, &[]), var(0)), app(app(var(2), var(1)), var(0))),
      ),
    );
    env.insert(
      rec_id.clone(),
      KConst::Recr {
        name: mk_name(&format!("{n}.rec")),
        level_params: vec![],
        k: false,
        is_unsafe: false,
        lvls: 0,
        params: 0,
        indices: 1,
        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(), ctor_id, rec_id]);
    check_rejects(&mut env, &block_id);
  }

  // ==========================================================================
  // Batch 14: Inductive with dup level params (Tutorial.lean 282–296)
  // ==========================================================================

  /// inductLevelParam: inductive with duplicate level params [u, u]
  #[test]
  fn bad_induct_dup_level_params() {
    let mut env = KEnv::<Meta>::new();
    let id = mk_simple_indc(
      &mut env,
      "inductLevelParam",
      2,                             // 2 level params
      &[mk_name("u"), mk_name("u")], // duplicate!
      &sort1(),
    );
    check_rejects(&mut env, &id);
  }