( obj: LeanBorrowed<'_>, cache: &mut Cache<'_>, )
| 756 | ) -> SyntaxPreresolved { |
| 757 | let p = LeanIxSyntaxPreresolved::from_ctor(obj.as_ctor()); |
| 758 | match p.as_ctor().tag() { |
| 759 | 0 => { |
| 760 | let name = decode_name(p.get_obj(0), cache.global); |
| 761 | SyntaxPreresolved::Namespace(name) |
| 762 | }, |
| 763 | 1 => { |
| 764 | let name = decode_name(p.get_obj(0), cache.global); |
| 765 | let fields: Vec<String> = p |
| 766 | .get_obj(1) |
| 767 | .as_list() |
| 768 | .iter() |
| 769 | .map(|o| o.as_string().to_string()) |
| 770 | .collect(); |
| 771 | SyntaxPreresolved::Decl(name, fields) |
| 772 | }, |
| 773 | tag => unreachable!("Invalid Lean.Syntax.Preresolved tag: {tag}"), |
| 774 | } |
| 775 | } |
| 776 | |
| 777 | fn decode_syntax(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>) -> Syntax { |
| 778 | if obj.is_scalar() { |
| 779 | return Syntax::Missing; |
| 780 | } |
| 781 | let s = LeanIxSyntax::from_ctor(obj.as_ctor()); |
| 782 | match s.as_ctor().tag() { |
| 783 | 1 => { |
| 784 | let info = decode_source_info(s.get_obj(0)); |
| 785 | let kind = decode_name(s.get_obj(1), cache.global); |
| 786 | let args: Vec<_> = s |
| 787 | .get_obj(2) |
| 788 | .as_array() |
| 789 | .iter() |
no test coverage detected