Function bad_induct_neg_reducible

crates/kernel/src/tutorial/inductive.rs:812–919

()

        level_params: vec![],
        lvls: 0,
        params: 0,
        indices: 0,
        is_unsafe: false,
        block: block_id.clone(),
        member_idx: 0,
        ty: sort1(),
        ctors: vec![ctor_id.clone()],
        lean_all: vec![block_id.clone()],
      },
    );

    // mk : (constType aType I → I) → I
    // constType aType I = aType (first arg), so field type is (aType → I)
    // But before reduction: constType aType I has I in head-normal form's first arg
    // The kernel checks HNF and sees I in the function domain = negative occurrence
    let ct_app =
      app(app(cnst("constType", &[]), cnst("aType", &[])), cnst(n, &[]));
    let field_ty = pi(ct_app, cnst(n, &[])); // (constType aType I) → I
    env.insert(
      ctor_id.clone(),
      KConst::Ctor {
        name: mk_name(&format!("{n}.mk")),
        level_params: vec![],
        is_unsafe: false,
        lvls: 0,
        induct: block_id.clone(),
        cidx: 0,
        params: 0,
        fields: 1,
        ty: pi(field_ty, cnst(n, &[])),
      },
    );

    let rec_ty = npi(
      "motive",
      pi(cnst(n, &[]), sort(param(0))),
      npi(
        "mk",
        pi(
          pi(
            pi(
              app(
                app(cnst("constType", &[]), cnst("aType", &[])),
                cnst(n, &[]),
              ),
              cnst(n, &[]),
            ),
            cnst(n, &[]),
          ),
          app(var(1), cnst(n, &[])),
        ),
        npi("t", cnst(n, &[]), app(var(2), var(0))),
      ),
    );
    env.insert(
      rec_id.clone(),
      KConst::Recr {
        name: mk_name(&format!("{n}.rec")),