Function quot_env

crates/kernel/src/whnf.rs:4522–4570

Minimal Quot env: Quot / Quot.mk / Quot.lift / Quot.ind as axioms.

()

    let char_ty = AE::cnst(prims.char_type.clone(), Box::new([]));
    let char_of_nat = AE::cnst(prims.char_of_nat.clone(), Box::new([]));
    let list_nil = AE::cnst(list_nil_id.clone(), Box::new([]));
    let list_cons = AE::cnst(list_cons_id.clone(), Box::new([]));
    let nil_char = app(list_nil, char_ty.clone());
    let char_a = app(char_of_nat, mk_nat(65));
    let one_char_list =
      apps_ae(list_cons, &[char_ty.clone(), char_a, nil_char]);
    env.insert(
      string_to_list_id.clone(),
      KConst::Defn {
        name: (),
        level_params: (),
        kind: DefKind::Definition,
        safety: DefinitionSafety::Safe,
        hints: ReducibilityHints::Regular(0),
        lvls: 0,
        ty: sort0(),
        val: lam(sort0(), one_char_list),
        lean_all: (),
        block: string_to_list_id.clone(),
      },
    );

    let nat_succ = AE::cnst(prims.nat_succ.clone(), Box::new([]));
    let motive = lam(sort0(), nat());
    let cons_case = lam(
      var(1),
      lam(app(list_const.clone(), var(2)), lam(nat(), app(nat_succ, var(0)))),
    );
    let length_body =
      apps_ae(rec_const, &[var(1), motive, mk_nat(0), cons_case, var(0)]);
    env.insert(
      list_length_id.clone(),
      KConst::Defn {
        name: (),
        level_params: (),
        kind: DefKind::Definition,
        safety: DefinitionSafety::Safe,
        hints: ReducibilityHints::Regular(0),
        lvls: 1,
        ty: sort0(),
        val: lam(sort0(), lam(app(list_const, var(0)), length_body)),
        lean_all: (),
        block: list_length_id.clone(),
      },
    );

    let mut tc = TypeChecker::new(&mut env);
    let string_to_list = AE::cnst(string_to_list_id, Box::new([]));
    let list_length = AE::cnst(list_length_id, Box::new([KUniv::zero()]));
    let nat_ble = AE::cnst(tc.prims.nat_ble.clone(), Box::new([]));

    let sample = " 0123abcABC:,;`\\/";