Function inline_like_env

crates/kernel/src/inductive.rs:5940–6177

Mimics Lean.Doc.Inline: parameterized type with Array nesting. Inl.{u} (i : Sort (u+1)) : Sort (u+1) Inl.text.{u} : ∀ (i : Sort (u+1)), String → Inl.{u} i Inl.emph.{u} : ∀ (i : Sort (u+1)), Array.{u+1} (Inl.{u} i) → Inl.{u} i Inl.other.{u} : ∀ (i : Sort (u+1)), i → Array.{u+1} (Inl.{u} i) → Inl.{u} i

()

      "Nat.succ rule should have 4 lambdas (0p + 1m + 2min + 1f), got {n_lams}"
    );
  }

  /// Build env with List (1 param, 2 ctors including recursive cons).
  /// List.{u} : Sort u → Sort u
  /// List.nil.{u} : ∀ (α : Sort u), List.{u} α
  /// List.cons.{u} : ∀ (α : Sort u), α → List.{u} α → List.{u} α
  fn list_env() -> KEnv<Anon> {
    let mut env = KEnv::new();
    let block = mk_id("List");

    // List : Sort u → Sort u  (1 lvl param)
    let list_ty = pi(AE::sort(param(0)), AE::sort(param(0)));
    env.insert(
      mk_id("List"),
      KConst::Indc {
        name: (),
        level_params: (),
        lvls: 1,
        params: 1,
        indices: 0,
        is_unsafe: false,
        block: block.clone(),
        member_idx: 0,
        ty: list_ty,
        ctors: vec![mk_id("List.nil"), mk_id("List.cons")],
        lean_all: (),
      },
    );

    // List.nil : ∀ (α : Sort u), List α
    let list_a = app(cnst("List", &[param(0)]), var(0)); // List.{u} α
    let nil_ty = pi(AE::sort(param(0)), list_a.clone());
    env.insert(
      mk_id("List.nil"),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 1,
        induct: mk_id("List"),
        cidx: 0,
        params: 1,
        fields: 0,
        ty: nil_ty,
      },
    );

    // List.cons : ∀ (α : Sort u) (head : α) (tail : List α), List α
    let cons_ty = pi(
      AE::sort(param(0)), // α
      pi(
        var(0), // head : α
        pi(
          app(cnst("List", &[param(0)]), var(1)), // tail : List α
          app(cnst("List", &[param(0)]), var(2)), // List α
        ),
      ),
    );