Function syntax_like_flat_block

crates/kernel/src/inductive.rs:5776–5797

()

      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 0,
        induct: mk_id("Nat"),
        cidx: 0,
        params: 0,
        fields: 0,
        ty: nat(),
      },
    );
    env.insert(
      mk_id("Nat.succ"),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 0,
        induct: mk_id("Nat"),
        cidx: 1,
        params: 0,
        fields: 1,
        ty: pi(nat(), nat()),
      },
    );