Decode a single (Name, ConstantInfo) pair.
( obj: LeanBorrowed<'_>, global: &GlobalCache, )
| 1058 | let kind = match inner.get_num_8(0) { |
| 1059 | 0 => QuotKind::Type, |
| 1060 | 1 => QuotKind::Ctor, |
| 1061 | 2 => QuotKind::Lift, |
| 1062 | 3 => QuotKind::Ind, |
| 1063 | b => unreachable!("Invalid QuotKind byte: {b}"), |
| 1064 | }; |
| 1065 | ConstantInfo::QuotInfo(QuotVal { cnst: constant_val, kind }) |
| 1066 | }, |
| 1067 | 5 => { |
| 1068 | let inner = LeanIxInductiveVal::from_ctor(inner_obj.as_ctor()); |
| 1069 | let constant_val = decode_constant_val(inner.get_obj(0), cache); |
| 1070 | let num_params = LeanNat::to_nat(&inner.get_obj(1)); |
| 1071 | let num_indices = LeanNat::to_nat(&inner.get_obj(2)); |
| 1072 | let all: Vec<_> = collect_list_borrowed(inner.get_obj(3).as_list()) |
| 1073 | .into_iter() |
| 1074 | .map(|o| decode_name(o, cache.global)) |
no test coverage detected