Function negative_self_function_env

crates/kernel/src/inductive.rs:6615–6658

(is_unsafe: bool)

        induct: mk_id("List"),
        cidx: 0,
        params: 1,
        fields: 0,
        ty: nil_ty,
      },
    );
    let cons_ty = pi(
      AE::sort(param(0)),
      pi(
        var(0),
        pi(
          app(cnst("List", &[param(0)]), var(1)),
          app(cnst("List", &[param(0)]), var(2)),
        ),
      ),
    );
    env.insert(
      mk_id("List.cons"),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 1,
        induct: mk_id("List"),
        cidx: 1,
        params: 1,
        fields: 2,
        ty: cons_ty,
      },
    );

    env.blocks.insert(
      block,
      vec![mk_id("PTree"), mk_id("PTree.leaf"), mk_id("PTree.node")],
    );
    env.blocks.insert(
      mk_id("List"),
      vec![mk_id("List"), mk_id("List.nil"), mk_id("List.cons")],
    );
    env
  }

  #[test]
  fn poly_nested_flat_block() {
    let mut env = poly_nested_env();
    let mut tc = TypeChecker::new(&mut env);
    // Check inductive first (consumes fuel for validation)
    tc.check_const(&mk_id("PTree")).unwrap();