Function nat_env

crates/kernel/src/tutorial/reduction.rs:460–607

Build N (Nat-like) environment with working recursor rules.

()

    let mut env = KEnv::<Meta>::new();
    let n = "N";
    let block_id = mk_id(n);
    let zero_id = mk_id("N.zero");
    let succ_id = mk_id("N.succ");
    let rec_id = mk_id("N.rec");

    let nat = || cnst(n, &[]);

    // N : Type
    env.insert(
      block_id.clone(),
      KConst::Indc {
        name: mk_name(n),
        level_params: vec![],
        lvls: 0,
        params: 0,
        indices: 0,
        is_unsafe: false,
        block: block_id.clone(),
        member_idx: 0,
        ty: sort1(),
        ctors: vec![zero_id.clone(), succ_id.clone()],
        lean_all: vec![block_id.clone()],
      },
    );

    // N.zero : N
    env.insert(
      zero_id.clone(),
      KConst::Ctor {
        name: mk_name("N.zero"),
        level_params: vec![],
        is_unsafe: false,
        lvls: 0,
        induct: block_id.clone(),
        cidx: 0,
        params: 0,
        fields: 0,
        ty: nat(),
      },
    );

    // N.succ : N → N
    env.insert(
      succ_id.clone(),
      KConst::Ctor {
        name: mk_name("N.succ"),
        level_params: vec![],
        is_unsafe: false,
        lvls: 0,
        induct: block_id.clone(),
        cidx: 1,
        params: 0,
        fields: 1,
        ty: pi(nat(), nat()),
      },
    );

    // N.rec : ∀ {motive : N → Sort u} (zero : motive N.zero)