Function decode_env

crates/ffi/src/lean_env.rs:1074–1109

Decode a Lean environment in parallel with hybrid caching.

(list: LeanList<LeanBorrowed<'_>>)

        cnst: constant_val,
        induct,
        cidx,
        num_params,
        num_fields,
        is_unsafe,
      })
    },
    7 => {
      let inner = LeanIxRecursorVal::from_ctor(inner_obj.as_ctor());
      let constant_val = decode_constant_val(inner.get_obj(0), cache);
      let all: Vec<_> = collect_list_borrowed(inner.get_obj(1).as_list())
        .into_iter()
        .map(|o| decode_name(o, cache.global))
        .collect();
      let num_params = LeanNat::to_nat(&inner.get_obj(2));
      let num_indices = LeanNat::to_nat(&inner.get_obj(3));
      let num_motives = LeanNat::to_nat(&inner.get_obj(4));
      let num_minors = LeanNat::to_nat(&inner.get_obj(5));
      let rules: Vec<_> = collect_list_borrowed(inner.get_obj(6).as_list())
        .into_iter()
        .map(|o| decode_recursor_rule(o, cache))
        .collect();
      let k = inner.get_num_8(0) != 0;
      let is_unsafe = inner.get_num_8(1) != 0;
      ConstantInfo::RecInfo(RecursorVal {
        cnst: constant_val,
        all,
        num_params,
        num_indices,
        num_motives,
        num_minors,
        rules,
        k,
        is_unsafe,
      })
    },
    tag => unreachable!("Invalid Lean.ConstantInfo tag: {tag}"),
  }
}