Method mk_ind_univs

crates/kernel/src/inductive.rs:3210–3219

Create shifted universe param args for an inductive in a recursor context. For large eliminators (offset=1): [Param(1), ..., Param(n)]. For small eliminators (offset=0): [Param(0), ..., Param(n-1)].

(&mut self, ind_lvls: u64, offset: u64)

              lift(&mut self.env.intern, &sp, lift_by as u64, 0)
            } else {
              sp
            }
          } else {
            let depth = self.depth();
            KExpr::var(depth - 1 - j, anon())
          };
          ty = subst(&mut self.env.intern, body, &p, 0);
        },
        _ => break,
      }
    }

    // Collect fields and push them as locals