( obj: LeanBorrowed<'_>, cache: &mut Cache<'_>, )
| 697 | return cached.clone(); |
| 698 | } |
| 699 | let level = if obj.is_scalar() { |
| 700 | Level::zero() |
| 701 | } else { |
| 702 | let l = LeanIxLevel::from_ctor(obj.as_ctor()); |
| 703 | match l.as_ctor().tag() { |
| 704 | 1 => Level::succ(decode_level(l.get_obj(0), cache)), |
| 705 | 2 => Level::max( |
| 706 | decode_level(l.get_obj(0), cache), |
| 707 | decode_level(l.get_obj(1), cache), |
| 708 | ), |
| 709 | 3 => Level::imax( |
| 710 | decode_level(l.get_obj(0), cache), |
| 711 | decode_level(l.get_obj(1), cache), |
| 712 | ), |
| 713 | 4 => Level::param(decode_name(l.get_obj(0), cache.global)), |
| 714 | 5 => Level::mvar(decode_name(l.get_obj(0), cache.global)), |
| 715 | tag => unreachable!("Invalid Lean.Level tag: {tag}"), |
| 716 | } |
| 717 | }; |
| 718 | cache.local.univs.insert(ptr, level.clone()); |
| 719 | level |
| 720 | } |
| 721 | |
| 722 | fn decode_substring(obj: LeanBorrowed<'_>) -> Substring { |
| 723 | let s = LeanIxSubstring::from_ctor(obj.as_ctor()); |
| 724 | let str = s.get_obj(0).as_string().to_string(); |
no test coverage detected